hasSum_coe — Mathlib

English

If f: α → NNReal has summable values, then ENNReal.ofNNReal (tsum f) equals the sum of ENNReal of f.

Русский

Если f: α → NNReal суммируема, то ENNReal.ofNNReal (tsum f) равен сумме ENNReal от f.

LaTeX

$$$\\text{HasSum}(f) \\Rightarrow \\text{ENNReal.ofNNReal} \\left(\\sum f\\right) = \\operatorname{tsum}_{a} (\\text{ENNReal.ofNNReal}(f(a))).$$$

Lean4

@[norm_cast]
protected theorem hasSum_coe {f : α → ℝ≥0} {r : ℝ≥0} : HasSum (fun a => (f a : ℝ≥0∞)) ↑r ↔ HasSum f r := by
  simp only [HasSum, ← coe_finset_sum, tendsto_coe]

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