4.1. Measurable Spaces🔗

Definition (Measurable Space).

Let X be a set. A sigma-algebra on X is a collection \mathcal{M} \subseteq \mathcal{P}(X) such that

\emptyset \in \mathcal{M},
if A \in \mathcal{M}, then A^c \in \mathcal{M},
if A_0, A_1, \dots \in \mathcal{M}, then \bigcup_{n \in \mathbb{N}} A_n \in \mathcal{M}.

A set X equipped with a sigma-algebra \mathcal{M} is called a measurable space.

Lean code

/-- A measurable space is a space equipped with a σ-algebra. -/
@[class] structure MeasurableSpace (α : Type*) where
  /-- Predicate saying that a given set is measurable. Use `MeasurableSet` in the root namespace
  instead. -/
  MeasurableSet' : Set α → Prop
  /-- The empty set is a measurable set. Use `MeasurableSet.empty` instead. -/
  measurableSet_empty : MeasurableSet' ∅
  /-- The complement of a measurable set is a measurable set. Use `MeasurableSet.compl` instead. -/
  measurableSet_compl : ∀ s, MeasurableSet' s → MeasurableSet' sᶜ
  /-- The union of a sequence of measurable sets is a measurable set. Use a more general
  `MeasurableSet.iUnion` instead. -/
  measurableSet_iUnion : ∀ f : ℕ → Set α, (∀ i, MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)

Definition (Measurable Set).

If X is a measurable space, its sigma-algebra is denoted by \mathcal{M}(X). A subset A \subseteq X is called measurable if A \in \mathcal{M}(X).

Lean code

/-- `MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`) -/
def MeasurableSet [MeasurableSpace α] (s : Set α) : Prop :=
  ‹MeasurableSpace α›.MeasurableSet' s

Definition (Measurable Map).

Let X and Y be measurable spaces. A function f : X \to Y is called measurable if for any measurable set B \subseteq Y, the preimage f^{-1}(B) \subseteq X is measurable.

Lean code

/-- A function `f` between measurable spaces is measurable if the preimage of every
  measurable set is measurable. -/
@[fun_prop]
def Measurable [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Prop :=
  ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)