ae_eq_of_forall_setIntegral_eq — Mathlib

English

If f and g are integrable and satisfy ∫_s f = ∫_s g for every finite-measure measurable set s, then f = g almost everywhere.

Русский

Если f и g интегрируемы и выполняется ∫_s f = ∫_s g для каждого измеримого множества s мерыfinite, то f = g почти повсюду.

LaTeX

$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$

Lean4

theorem ae_eq_of_forall_setIntegral_eq (f g : α → E) (hf : Integrable f μ) (hg : Integrable g μ)
    (hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) : f =ᵐ[μ] g :=
  by
  rw [← sub_ae_eq_zero]
  have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 :=
    by
    intro s hs hμs
    rw [integral_sub' hf.integrableOn hg.integrableOn]
    exact sub_eq_zero.mpr (hfg s hs hμs)
  exact Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero (hf.sub hg) hfg'

Похожие утверждения