6.1. ほとんど至る所
X を可測空間とし、\mu を X 上の測度とします。
定義.
P(x) を点 x \in X に関する性質とする。
P が \mu に関して ほとんど至る所 成り立つ
（あるいは P(x) が \mu-a.e. x \in X で成り立つ）とは、
例外集合の外測度が 0 であること、すなわち
\mu^* (\{x \in X \mid \neg P(x)\}) = 0
が成り立つことをいう。
ここで \mu^{*} は\mu に
付随する外測度
を表す。
Lean code
theorem ae_iff {p : α → Prop} : (∀ᵐ a ∂μ, p a) ↔ μ { a | ¬p a } = 0 :=
Iff.rfl
補題.
f, g : X \to [0,\infty] とする。
f = g がほとんど至る所成り立つならば、それらの下ルベーグ積分は等しい:
\underline{\int}_{x \in X} f(x)\,d\mu
=
\underline{\int}_{x \in X} g(x)\,d\mu.
Lean code
theorem SimpleFunc.measure_preimage_singleton_congr_ae (f g : SimpleFunc X)
(hfg : ∀ᵐ x ∂μ, f x = g x) (y : ℝ≥0∞) :
μ (f ⁻¹' {y}) = μ (g ⁻¹' {y}) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
have hnull : μ {x | f x ≠ g x} = 0 := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
All goals completed! 🐙
have hfg_diff : μ (f ⁻¹' {y} \ g ⁻¹' {y}) = 0 := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
All goals completed! 🐙
have hgf_diff : μ (g ⁻¹' {y} \ f ⁻¹' {y}) = 0 := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞hnull:μ {x | f x ≠ g x} = 0 := id (Eq.mp measure_preimage_singleton_congr_ae._simp_1 hfg)hfg_diff:μ (⇑f ⁻¹' {y} \ ⇑g ⁻¹' {y}) = 0 := measure_mono_null (preimage_singleton_diff_subset_setOf_ne (⇑f) (⇑g) y) hnull⊢ μ {x | g x ≠ f x} = 0
All goals completed! 🐙
All goals completed! 🐙theorem lintegral_mono_ae {f g : X → ℝ≥0∞} (hfg : ∀ᵐ x ∂μ, f x ≤ g x) :
∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
have h_ae_not_mem : ∀ᵐ x ∂μ, x ∉ t := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun x => g x), g_1.lintegral μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ ⇑(s.restrict tᶜ) ≤ fun x => g xX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ ⇑(s.restrict tᶜ) ≤ fun x => g x X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:X⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) xX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ 0 ≤ (fun x => g x) x
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x have hsxg : s x ≤ g x := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ thsxg:s x ≤ g x := le_trans (hsf x) (by_contra fun hxfg => hx (hts hxfg))⊢ s x ≤ (fun x => g x) x
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ have h_restrict : ∀ᵐ x ∂μ, s x = s.restrict tᶜ x := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
exact h_ae_not_mem.mono fun x hxt ↦ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t :=
Eq.mpr
(id
(Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
(congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhxt:x ∉ t⊢ s x = (s.restrict tᶜ) x
All goals completed! 🐙
All goals completed! 🐙theorem lintegral_congr_ae {f g : X → ℝ≥0∞} (hfg : ∀ᵐ x ∂μ, f x = g x) :
∫⁻ x, f x ∂μ = ∫⁻ x, g x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ = ∫⁻ (x : X), g x ∂μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), g x ∂μ ≤ ∫⁻ (x : X), f x ∂μ
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), g x ∂μ ≤ ∫⁻ (x : X), f x ∂μ All goals completed! 🐙