hasFiniteIntegral_count_iff — Mathlib

English

For a unit c in a normed ring 𝕜, HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ.

Русский

Для единицы c в нормированном кольце 𝕜 имеем: HasFiniteIntegral (c • f) μ ⇔ HasFiniteIntegral f μ.

LaTeX

$$$IsUnit c \Rightarrow (HasFiniteIntegral (c \cdot f) μ \iff HasFiniteIntegral f μ)$$$

Lean4

/-- A function has finite integral for the counting measure iff its norm is summable. -/
theorem hasFiniteIntegral_count_iff {f : α → β} : HasFiniteIntegral f Measure.count ↔ Summable (‖f ·‖) := by
  simp only [hasFiniteIntegral_iff_enorm, enorm, lintegral_count, lt_top_iff_ne_top, tsum_coe_ne_top_iff_summable,
    ← summable_coe, coe_nnnorm]

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