English
Under sigma-finite μ, if the integrals of f over every measurable set s coincide with those of g, then f = g almost everywhere.
Русский
При сигма-конечной μ, если интегралы f по всем измеримым множествам совпадают с интегралами g, то f = g a.e.
LaTeX
$$$f = g \ a.e. \ μ$ whenever $\int_s f = \int_s g$ for all measurable s.$$
Lean4
theorem ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E}
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) (hf : AEFinStronglyMeasurable f μ) :
f =ᵐ[μ] 0 := by
let t := hf.sigmaFiniteSet
suffices f =ᵐ[μ.restrict t] 0 from ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl
haveI : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict
refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_
· intro s hs hμs
rw [IntegrableOn, Measure.restrict_restrict hs]
rw [Measure.restrict_apply hs] at hμs
exact hf_int_finite _ (hs.inter hf.measurableSet) hμs
· intro s hs hμs
rw [Measure.restrict_restrict hs]
rw [Measure.restrict_apply hs] at hμs
exact hf_zero _ (hs.inter hf.measurableSet) hμs
