測度空間と可測集合

可測空間構造は MeasurableSpace α です． 測度は Measure α で，可測集合だけでなく任意の集合 s : Set α に対して μ s : ℝ≥0∞ が定義されています． ただし，多くの定理では可測性の仮定が必要です．

#check MeasurableSpace
#check Measure
#check MeasurableSet
#check (fun {α : Type*} [MeasurableSpace α] => Measure α)

section MeasurableSets

variable {α : Type*} [MeasurableSpace α]

example : MeasurableSet (∅ : Set α) := by
  exact MeasurableSet.empty

example : MeasurableSet (univ : Set α) := by
  exact MeasurableSet.univ

example {s : Set α} (hs : MeasurableSet s) : MeasurableSet sᶜ := by
  exact hs.compl

variable {ι : Type*} [Encodable ι]

example {f : ι → Set α} (h : ∀ i, MeasurableSet (f i)) :
    MeasurableSet (⋃ i, f i) := by
  exact MeasurableSet.iUnion h

example {f : ι → Set α} (h : ∀ i, MeasurableSet (f i)) :
    MeasurableSet (⋂ i, f i) := by
  exact MeasurableSet.iInter h

end MeasurableSets

可算和や可算共通部分には，添字型が可算であることが必要です． 上の例では [Encodable ι] によって，ι が可算に符号化できることを仮定しています．

演習問題

1. 可測集合の補集合が可測であることを示してください．

   example {α : Type*} [MeasurableSpace α] {s : Set α}
       (hs : MeasurableSet s) : MeasurableSet sᶜ := by
     -- ヒント: `exact hs.compl`
     sorry
   

2. MeasurableSet.iUnion の仮定を読み，可算性がどこで必要か確認してください．

   #check MeasurableSet.iUnion