isLittleO_sum_range_of_tendsto_zero

English

If f → 0 along atTop, then the sum over range n of f is little-o of n, i.e., it is small compared to n.

Русский

Если f(n) → 0 при n → ∞, то сумма по диапазону до n функции f является little-o от n.

LaTeX

$$$\bigl(\sum_{i=0}^{n-1} f(i)\bigr) = o_{atTop} n$ when $f \to 0$ atTop$$

Lean4

theorem isLittleO_sum_range_of_tendsto_zero {α : Type*} [NormedAddCommGroup α] {f : ℕ → α} (h : Tendsto f atTop (𝓝 0)) :
    (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => (n : ℝ) :=
  by
  have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
  simp only [sum_const, card_range, Nat.smul_one_eq_cast] at this
  exact this tendsto_natCast_atTop_atTop

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