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]