測度

測度 μ : Measure α は集合に ℝ≥0∞ の値を割り当てます． ℝ≥0∞ は拡張非負実数で，無限大 ∞ を含みます．

#check ENNReal
#check (∞ : ℝ≥0∞)
#check MeasureTheory.Measure
#check measure_iUnion_le

section Measures

variable {α : Type*} [MeasurableSpace α]
variable {μ : Measure α}

example (s : Set α) : μ s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), μ t := by
  exact measure_eq_iInf s

example {ι : Type*} [Encodable ι] (s : ι → Set α) :
    μ (⋃ i, s i) ≤ ∑' i, μ (s i) := by
  exact measure_iUnion_le s

example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in ae μ, P x := by
  rfl

end Measures

∀ᵐ x ∂μ, P x は「μ に関してほとんど至る所 P x が成り立つ」という意味です． これはフィルター ae μ による Eventually の記法です．

演習問題

ほとんど至る所の記法 ∀ᵐ が filter の Eventually であることを確認してください．

example {α : Type*} [MeasurableSpace α] {μ : Measure α} {P : α → Prop} :
    (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in ae μ, P x := by
  -- ヒント: `rfl`
  sorry