English
In a sigma-finite setting, for f,g : α → F', if all integrals over measurable sets match, then f = a.e. g.
Русский
При сигма-финости, если интегралы по всем измеримым множествам совпадают для f и g, то f = a.e. g.
LaTeX
$$$$ f =_{a.e.} g $$$$
Lean4
theorem ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] {f g : α → F'}
(hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
(hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
(hfg_eq : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
(hfm : AEStronglyMeasurable[m] f μ) (hgm : AEStronglyMeasurable[m] g μ) : f =ᵐ[μ] g :=
by
rw [← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm]
have hf_mk_int_finite (s) : MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hfm.mk f) s (μ.trim hm) :=
by
intro hs hμs
rw [trim_measurableSet_eq hm hs] at hμs
rw [IntegrableOn, restrict_trim hm _ hs]
refine Integrable.trim hm ?_ hfm.stronglyMeasurable_mk
exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.ae_eq_mk)
have hg_mk_int_finite (s) : MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hgm.mk g) s (μ.trim hm) :=
by
intro hs hμs
rw [trim_measurableSet_eq hm hs] at hμs
rw [IntegrableOn, restrict_trim hm _ hs]
refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk
exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)
have hfg_mk_eq :
∀ s : Set α,
MeasurableSet[m] s → μ.trim hm s < ∞ → ∫ x in s, hfm.mk f x ∂μ.trim hm = ∫ x in s, hgm.mk g x ∂μ.trim hm :=
by
intro s hs hμs
rw [trim_measurableSet_eq hm hs] at hμs
rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
integral_trim hm hgm.stronglyMeasurable_mk, integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
exact hfg_eq s hs hμs
exact ae_eq_of_forall_setIntegral_eq_of_sigmaFinite hf_mk_int_finite hg_mk_int_finite hfg_mk_eq
