tsum_eq_limsup_sum_nat — Mathlib

English

For f : ℕ → ENNReal, the total sum equals the limsup of the sequence of partial sums: ∑' i, f i = limsup (n → ∞) ∑_{i ∈ Finset.range n} f i.

Русский

Для f : ℕ → ENNReal сумма равна limsup последовательности частичных сумм: ∑' i, f i = limsup_{n→∞} ∑_{i=0}^{n-1} f(i).

LaTeX

$$$\sum_{i \in \mathbb{N}}' f(i) = \limsup_{n \to \infty} \sum_{i=0}^{n-1} f(i)$$$

Lean4

protected theorem tsum_eq_limsup_sum_nat {f : ℕ → ℝ≥0∞} :
    ∑' i, f i = limsup (fun n => ∑ i ∈ Finset.range n, f i) atTop :=
  ENNReal.summable.hasSum.tendsto_sum_nat.limsup_eq.symm

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