English
Let f and g be elements of Lp E p μ with p ≠ 0 and p ≠ ∞. If the integrals of f and g over every finite-measure measurable set agree, then f = g almost everywhere.
Русский
Пусть f и g принадлежат Lp(E, p, μ) с p ≠ 0 и p ≠ ∞. Если интегралы f и g по всем измеримым множествам конечной меры совпадают, то f = g почти повсюду.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} g, $$$$
Lean4
theorem ae_eq_of_forall_setIntegral_eq (f g : Lp E p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hg_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn g s μ)
(hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) : f =ᵐ[μ] g :=
AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq hf_int_finite hg_int_finite hfg
(Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top).aefinStronglyMeasurable
(Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top).aefinStronglyMeasurable
