lintegral_eq_iSup_eapprox_lintegral

English

For a measurable f: α → ℝ≥0∞, the integral equals the iSup of the lintegrals of the approximants eapprox f n.

Русский

Для измеримой функции f интеграл равен sup-пределу интегралов приближений eapprox f n.

LaTeX

$$$$ \\int^{\\!-}_{a} f(a) \\, d\\mu = \\bigvee_{n} (eapprox f n).lintegral \\mu. $$$$

Lean4

theorem lintegral_eq_iSup_eapprox_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ a, f a ∂μ = ⨆ n, (eapprox f n).lintegral μ :=
  calc
    ∫⁻ a, f a ∂μ = ∫⁻ a, ⨆ n, (eapprox f n : α → ℝ≥0∞) a ∂μ := by congr; ext a; rw [iSup_eapprox_apply hf]
    _ = ⨆ n, ∫⁻ a, (eapprox f n : α → ℝ≥0∞) a ∂μ :=
      by
      apply lintegral_iSup
      · fun_prop
      · intro i j h
        exact monotone_eapprox f h
    _ = ⨆ n, (eapprox f n).lintegral μ := by congr; ext n; rw [(eapprox f n).lintegral_eq_lintegral]

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