hasFiniteIntegral_toReal_iff — Mathlib

English

For f: α → ENNReal, if f is finite almost everywhere, then HasFiniteIntegral (fun x ↦ (f x).toReal) μ is equivalent to ∫⁻ x f x ∂μ ≠ ∞.

Русский

Для f: α → ENNReal, если почти везде f конечна, то HasFiniteIntegral (f x).toReal эквивалентно ∫⁻ f ≠ ∞.

LaTeX

$$$\forall f: α → ENNReal, (∀ᵐ x, f(x) ≠ ∞) \Rightarrow HasFiniteIntegral (x \mapsto (f x).toReal) μ \iff ∫⁻ x, f x ∂μ ≠ ∞$$$

Lean4

theorem hasFiniteIntegral_toReal_iff {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x ≠ ∞) :
    HasFiniteIntegral (fun x ↦ (f x).toReal) μ ↔ ∫⁻ x, f x ∂μ ≠ ∞ :=
  by
  have : ∀ᵐ x ∂μ, .ofReal (f x).toReal = f x := by filter_upwards [hf] with x hx; simp [hx]
  simp [hasFiniteIntegral_iff_enorm, Real.enorm_of_nonneg ENNReal.toReal_nonneg, lintegral_congr_ae this,
    lt_top_iff_ne_top]

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