summable_iff_not_tendsto_nat_atTop_of_nonneg

English

For nonnegative f, summability of f is equivalent to the negation of the tendsto of its partial sums to top.

Русский

Для неотрицательных f суммируемость эквивалентна неустойчивости пределов частичных сумм.

LaTeX

$$Summable f \\\\iff \\\\ neg\\\\ Tendsto (fun n => (Finset.range n).sum (fun i => f i)) atTop atTop$$

Lean4

theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
    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_of_nonneg hf]

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