lintegral_ofReal_ne_top_iff_integrable

English

For f: α→ℝ, AEStronglyMeasurable and f≥0 a.e., ∫ ENNReal.ofReal f ≠ ∞ iff f is integrable.

Русский

Для f: α→ℝ измеримого по Лемме и f≥0 почти всюду, линтеграл ≠ ∞ эквивалентен интегрируемости.

LaTeX

$$lintegral μ (fun x => ENNReal.ofReal (f x)) ≠ ∞ ↔ Integrable f μ$$

Lean4

theorem lintegral_ofReal_ne_top_iff_integrable {f : α → ℝ} (hfm : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) :
    ∫⁻ a, ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ Integrable f μ :=
  by
  rw [Integrable, hasFiniteIntegral_iff_ofReal hf]
  simp [hfm]

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