lintegral_eapprox_le_lintegral — Mathlib

English

For measurable f and n, the lintegral of eapprox f n is bounded above by the lintegral of f.

Русский

Для измеримой f и натурального n неравенство: (eapprox f n).lintegral ≤ f.lintegral.

LaTeX

$$$$ (eapprox f n).lintegral \\mu \\le \\int^{\\!-}_{x} f(x) \\; d\\mu. $$$$

Lean4

theorem lintegral_eapprox_le_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) (n : ℕ) :
    (eapprox f n).lintegral μ ≤ ∫⁻ x, f x ∂μ :=
  by
  rw [lintegral_eq_iSup_eapprox_lintegral hf]
  exact le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

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