integrable_toReal_iff — Mathlib

English

For ENNReal-valued f that is a.e.-finite, Integrable f in μ implies lintegral of f is finite and conversely.

Русский

Для f, принимающего значения ENNReal и конечного почти всюду, интегрируемость эквивалентна конечности линтеграла.

LaTeX

$$Integrable f μ ↔ (lintegral μ f ≠ ∞)$$

Lean4

theorem integrable_toReal_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
    Integrable (fun x ↦ (f x).toReal) μ ↔ ∫⁻ x, f x ∂μ ≠ ∞ :=
  by
  rw [Integrable, hasFiniteIntegral_toReal_iff hf_ne_top]
  simp only [hf.ennreal_toReal.aestronglyMeasurable, ne_eq, true_and]

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