English
If f,g are integrable and the setwise integrals ∫_s f and ∫_s g agree for all measurable s, then f=g a.e.
Русский
Если f,g интегрируемы и их интегралы по всем измеримым множествам совпадают, то f=g a.e.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$
Lean4
theorem ae_eq_of_forall_setLIntegral_eq {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(hfi : ∫⁻ x, f x ∂μ ≠ ∞) (hgi : ∫⁻ x, g x ∂μ ≠ ∞)
(hfg : ∀ ⦃s⦄, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) : f =ᵐ[μ] g :=
by
have hf' : AEFinStronglyMeasurable f μ := ENNReal.aefinStronglyMeasurable_of_aemeasurable hfi hf
have hg' : AEFinStronglyMeasurable g μ := ENNReal.aefinStronglyMeasurable_of_aemeasurable hgi hg
let s := hf'.sigmaFiniteSet
let t := hg'.sigmaFiniteSet
suffices f =ᵐ[μ.restrict (s ∪ t)] g
by
refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
simp only [Set.compl_union]
have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
filter_upwards [h1, h2] with x h1 h2 hx
rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.restrict hg.restrict fun u hu huμ ↦ ?_
rw [Measure.restrict_restrict hu]
rw [Measure.restrict_apply hu] at huμ
exact hfg (hu.inter (hf'.measurableSet.union hg'.measurableSet)) huμ
