English
For f : ℕ → ENNReal and a tendencied sequence N : ℕ → ℕ with Tendsto N atTop atTop, the total sum equals the supremum of sums over finite prefixes: ∑' i, f(i) = ⨆ i, ∑_{a ∈ Finset.range (N i)} f(a).
Русский
Для f : ℕ → ENNReal и нормирующей последовательности N : ℕ → ℕ с Tendsto N atTop atTop, сумма равна наибольшему пределу сумм по конечным префиксам: ∑' i, f(i) = ⨆ i, ∑_{a ∈ [0, N(i) - 1]} f(a).
LaTeX
$$$\sum'_{i \in \mathbb{N}} f(i) = \big\lbrace \sum_{a \in \mathrm{Finset.range}(N(i))} f(a) : i \in \mathbb{N} \big\rbrace^{\uparrow}$$$
Lean4
protected theorem tsum_eq_iSup_nat' {f : ℕ → ℝ≥0∞} {N : ℕ → ℕ} (hN : Tendsto N atTop atTop) :
∑' i : ℕ, f i = ⨆ i : ℕ, ∑ a ∈ Finset.range (N i), f a :=
ENNReal.tsum_eq_iSup_sum' _ fun t =>
let ⟨n, hn⟩ := t.exists_nat_subset_range
let ⟨k, _, hk⟩ := exists_le_of_tendsto_atTop hN 0 n
⟨k, Finset.Subset.trans hn (Finset.range_mono hk)⟩
