dist_partial_sum_le_of_le_geometric

English

If a function f satisfies a geometric bound, then the distance between partial sums satisfies a similar geometric estimate.

Русский

Если f удовлетворяет геометрическому ограничению, то расстояние между частичными суммами удовлетворяет аналогичному геометрическому неравенству.

LaTeX

$$dist(∑_{i=0}^{n-1} f(i), ∑_{i=0}^{n} f(i)) ≤ C r^{n}$$

Lean4

theorem dist_partial_sum_le_of_le_geometric (hf : ∀ n, ‖f n‖ ≤ C * r ^ n) (n : ℕ) :
    dist (∑ i ∈ range n, f i) (∑ i ∈ range (n + 1), f i) ≤ C * r ^ n :=
  by
  rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel_left]
  exact hf n

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