tsum_coe_ne_top_iff_summable — Mathlib

English

For f : β → NNReal, (∑' b, ENNReal.ofNNReal (f b)) ≠ ∞ if and only if f is summable.

Русский

Для f: β → NNReal, сумма ENNReal.fromNNReal (f b) не бесконечна тогда и только тогда, когда f суммируема.

LaTeX

$$$(\\sum' b, (f b)) ≠ \\infty \\iff \\text{Summable } f$ (in NNReal sense, transferred via ENNReal).$$

Lean4

theorem tsum_coe_ne_top_iff_summable {f : β → ℝ≥0} : (∑' b, (f b : ℝ≥0∞)) ≠ ∞ ↔ Summable f :=
  by
  refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩
  lift ∑' b, (f b : ℝ≥0∞) to ℝ≥0 using h with a ha
  refine ⟨a, ENNReal.hasSum_coe.1 ?_⟩
  rw [ha]
  exact ENNReal.summable.hasSum

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