not_summable_iff_tendsto_nat_atTop_of_nonneg

English

For nonnegative f: ℕ → ℝ, not summable is equivalent to the partial sums tending to +∞.

Русский

Для неотрицательных f: ℕ → ℝ не суммируемость эквивалентна тому, что частичные суммы стремятся к +∞.

LaTeX

$$$$\\neg\\operatorname{Summable} f \\ \\iff\\ \\operatorname{Tendsto}\\big(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\big)\\,\\text{atTop atTop}.$$$$

Lean4

theorem not_summable_iff_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
  lift f to ℕ → ℝ≥0 using hf
  simpa using mod_cast NNReal.not_summable_iff_tendsto_nat_atTop

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