MeasureTheory.OuterMeasure.AE
このファイルでは外測度の零集合の補集合s ∈ ae μ ↔ μ sᶜ = 0を定義しています.
/-- The “almost everywhere” filter of co-null sets. -/
def ae (μ : F) : Filter α :=
.ofCountableUnion (μ · = 0) (fun _S hSc ↦ (measure_sUnion_null_iff hSc).2) fun _t ht _s hs ↦
measure_mono_null hs ht
/-- `∀ᵐ a ∂μ, p a` means that `p a` for a.e. `a`, i.e. `p` holds true away from a null set.
This is notation for `Filter.Eventually p (MeasureTheory.ae μ)`. -/
notation3 "∀ᵐ "(...)" ∂"μ", "r:(scoped p => Filter.Eventually p <| MeasureTheory.ae μ) => r
measure_sUnion_null_iffとはMeasureTheory.OuterMeasure.Basicで, Filter.ofCountableUnionはOrder.Filter.CountableInterで定義されています. それぞれについてコードを見ることでaeの定義を理解しましょう.
theorem measure_sUnion_null_iff {S : Set (Set α)} (hS : S.Countable) :
μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0 := by
rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]
theorem measure_mono_null (h : s ⊆ t) (ht : μ t = 0) : μ s = 0 :=
eq_bot_mono (measure_mono h) ht
measure_sUnion_null_iffは可算個の集合の合併が零集合であることと, 各集合が零集合であることが同値であることを示しています. measure_mono_nullは包含関係と零集合の条件から, 零集合であることを示しています.
/-- Construct a filter with countable intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property. -/
def Filter.ofCountableInter (l : Set (Set α))
(hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
(h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
sets := l
univ_sets := @sInter_empty α ▸ hl _ countable_empty (empty_subset _)
sets_of_superset := h_mono _ _
inter_sets {s t} hs ht := sInter_pair s t ▸
hl _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
/-- Construct a filter with countable intersection property.
Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
Similarly to `Filter.ofCountableInter`,
this constructor deduces some properties from the countable intersection property
which becomes the countable union property because we take complements of all sets. -/
def Filter.ofCountableUnion (l : Set (Set α))
(hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l)
(hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α := by
refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
· rw [mem_setOf_eq, compl_sInter]
apply hUnion (compl '' S) (hSc.image _)
intro s hs
rw [mem_image] at hs
rcases hs with ⟨t, ht, rfl⟩
apply hSp ht
· rw [mem_setOf_eq]
rw [← compl_subset_compl] at hsub
exact hmono sᶜ ht tᶜ hsub
Filter.ofCountableInterとFilter.CountableUnionは包含関係について逆の関係になっています. Filter.CountableUnionは要素である集合の補集合を要素とする集合族がFilter.ofCountableInterを満たすことを示すことによって証明されます.
Filter.ofCountableInterは可算交叉の性質を持ち(hUnion), 上方向に閉じて(hmono)いる時, それはフィルタであることを示しています. つまりaeは可算交叉の性質を持っていることに注意してください.
aeの型を確認してみましょう. (μ · = 0)はSet α → Prop, (fun _S hSc ↦ (measure_sUnion_null_iff hSc).2)は∀ (_S : Set (Set α)), _S.Countable → (∀ s ∈ _S, μ s = 0) → μ (⋃₀ _S) = 0, fun _t ht _s hs ↦ measure_mono_null hs htは∀ _t ∈ fun x ↦ μ x = 0, ∀ _s ⊆ _t, μ _s = 0という型を持っています. 一見これはFilter.CountableUnionに合致していないように見えますが, Setの型が
def Set (α : Type u) := α → Prop
で特性関数と同一視する形で定義されているので, 実際はFilter.CountableUnionの型を満たしています.
theorem ae_of_all {p : α → Prop} (μ : F) : (∀ a, p a) → ∀ᵐ a ∂μ, p a :=
Eventually.of_forall
∀ᵐ a ∂μ, p aは{a | p a} ∈ ae μと定義されることに注意すると,Eventually.of_forallにより直接従います.
/-- `f =ᵐ[μ] g` means `f` and `g` are eventually equal along the a.e. filter,
i.e. `f=g` away from a null set.
This is notation for `Filter.EventuallyEq (MeasureTheory.ae μ) f g`. -/
notation:50 f " =ᵐ[" μ:50 "] " g:50 => Filter.EventuallyEq (MeasureTheory.ae μ) f g
ほとんど至る所でf = gであることをf =ᵐ[μ] gと略記して書きます.