hasFiniteIntegral_iff_ofNNReal — Mathlib

English

For real-valued f ≥ 0 a.e., HasFiniteIntegral f μ iff ∫ ENNReal.ofReal f dμ < ∞.

Русский

Для неотрицательной по мере f вещественной величины: HasFiniteIntegral f μ эквивалично ∫ ENNReal.ofReal f dμ < ∞.

LaTeX

$$$ \\text{HasFiniteIntegral} f \\mu \\iff \\int^- a \\, \\mathrm{ENNReal.ofReal}(f(a)) \\, d\\mu(a) < \\infty $$$

Lean4

theorem hasFiniteIntegral_iff_ofNNReal {f : α → ℝ≥0} : HasFiniteIntegral (fun x => (f x : ℝ)) μ ↔ (∫⁻ a, f a ∂μ) < ∞ :=
  by simp [hasFiniteIntegral_iff_norm]

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