ofReal_tsum_of_nonneg — Mathlib

English

If a real-valued sequence f is summable, then the tsum of its real-to-ENNReal images matches the tsum of those images.

Русский

Если последовательность f действительно суммируема, то сумма ENNReal(ofReal f(i)) равна сумме ofReal(f(i)).

LaTeX

$$$\text{Summable}(f) \Rightarrow \mathrm{ENNReal}.ofReal\left(\sum_i f(i)\right) = \sum_i \mathrm{ENNReal}.ofReal(f(i)).$$$

Lean4

theorem ofReal_tsum_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : Summable f) :
    ENNReal.ofReal (∑' n, f n) = ∑' n, ENNReal.ofReal (f n) := by
  simp_rw [ENNReal.ofReal, ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)]

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