ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite

English

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

Русский

Если μ сигма-конечна и f,g: α→ℝ≥0∞ являются AEMеасeable и их интегралы по всем конечным множествам совпадают, то f=g a.e.

LaTeX

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

Lean4

theorem ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : Measurable f)
    (hg : Measurable g) (h : ∀ s, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) : f =ᵐ[μ] g :=
  ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.aemeasurable hg.aemeasurable h

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