tsum_eq_liminf_sum_nat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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