hasSum_real_toNNReal_of_nonneg — Mathlib

English

If f: α → ℝ is nonnegative, and f is summable, then the NNReal-valued sum of f converges to the NNReal of the real sum.

Русский

Если f: α → ℝ неотрицательно и суммируема, то сумма в NNReal сходится к NNReal суммы в ℝ.

LaTeX

$$HasSum (λ n, (f n).toNNReal) (∑' f) .toNNReal$$

Lean4

theorem hasSum_real_toNNReal_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : Summable f L) :
    HasSum (fun n => Real.toNNReal (f n)) (Real.toNNReal (∑'[L] n, f n)) L :=
  hf.hasSum.toNNReal hf_nonneg

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