ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀

English

If μ is sigma-finite and f,g: α→ℝ≥0∞ are AEMeasurable with a.e. equality of all rectangle integrals, then f=g a.e.

Русский

Если μ сигма- сконечного типа, и f,g — AEMeasurable, равенство интегралов по всем прямоугольникам ведет к равенству a.e.

LaTeX

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

Lean4

theorem ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) (h : ∀ s, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) : f =ᵐ[μ] g :=
  by
  have A : f ≤ᵐ[μ] g := ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf fun s hs h's => le_of_eq (h s hs h's)
  have B : g ≤ᵐ[μ] f := ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hg fun s hs h's => ge_of_eq (h s hs h's)
  filter_upwards [A, B] with x using le_antisymm

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