summable_iff_not_tendsto_nat_atTop

English

Summable f is equivalent to not Tendsto of partial sums to atTop.

Русский

Суммируемость f эквивалентна тому, что частичные суммы не стремятся к некоторому пределу.

LaTeX

$$$\\\\forall f : \\\\mathbb{N} \\rightarrow \\\\mathbb{R}_{\\\\ge 0}, \\\\mathrm{Summable}(f) \\\\iff \\\\neg \\\\mathrm{Tendsto}\\left(n \\mapsto \\\\sum_{i=0}^{n-1} f(i)\\\\right) atTop atTop$$$

Lean4

theorem summable_iff_not_tendsto_nat_atTop {f : ℕ → ℝ≥0} :
    Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop := by
  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]

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