4.1. 可測空間
定義 (可測空間).
X を集合とする。
X 上の σ-代数とは、\mathcal{P}(X) の部分集合 \mathcal{M} \subseteq \mathcal{P}(X) であって、次を満たすものをいう。
-
\emptyset \in \mathcal{M}である。 -
A \in \mathcal{M}ならばA^c \in \mathcal{M}である。 -
A_0, A_1, \dots \in \mathcal{M}ならば\bigcup_{n \in \mathbb{N}} A_n \in \mathcal{M}である。
σ-代数 \mathcal{M} を備えた集合 X を 可測空間 という。
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)
定義 (可測集合).
X を可測空間とする。
その σ-代数を \mathcal{M}(X) と書く。
部分集合 A \subseteq X が 可測 であるとは、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
定義 (可測写像).
X と Y を可測空間とする。
写像 f : X \to Y が 可測 であるとは、任意の可測集合 B \subseteq Y に対して、その逆像
f^{-1}(B) \subseteq X が可測であることをいう。
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)