tsum_eq_toNNReal_tsum — Mathlib

English

The NNReal tsum equals the toNNReal of the ENNReal tsum, i.e., sums commute with the coercion to NNReal.

Русский

Сумма NNReal равна toNNReal суммы ENNReal через преобразование.

LaTeX

$$$\\sum' b, f b = (\\sum' b, (f b: \\mathbb{R}_{\\ge 0})).toNNReal$$$

Lean4

theorem tsum_eq_toNNReal_tsum {f : β → ℝ≥0} : ∑' b, f b = (∑' b, (f b : ℝ≥0∞)).toNNReal :=
  by
  by_cases h : Summable f
  · rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]
  · have A := tsum_eq_zero_of_not_summable h
    simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h
    simp only [h, ENNReal.toNNReal_top, A]

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