hasFiniteIntegral_iff_ofReal — Mathlib

English

The L1 map is linear with respect to scalar multiplication (variant version): toL1 (k • f) hf = k • toL1 f hf.

Русский

Линейность отображения L1 по скаляру (вариант): toL1(k • f) = k • toL1(f).

LaTeX

$$$ \\mathrm{toL1}(k \\cdot f) = k \\cdot \\mathrm{toL1}(f) $$$

Lean4

theorem hasFiniteIntegral_iff_ofReal {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) :
    HasFiniteIntegral f μ ↔ (∫⁻ a, ENNReal.ofReal (f a) ∂μ) < ∞ := by
  rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]

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