dist_le_range_sum_of_dist_le — Mathlib

English

A version of the previous bound where you are given an upper bound d_k for each intermediate distance dist(f(k), f(k+1)). Then dist(f(0), f(n)) ≤ ∑_{i=0}^{n-1} d_i.

Русский

Версия границы, когда для каждого промежуточного расстояния dist(f(k), f(k+1)) задано верхнее значение d_k; тогда dist(f(0), f(n)) ≤ ∑_{i=0}^{n-1} d_i.

LaTeX

$$$\\forall n,\\ \\mathrm{dist}(f(0), f(n)) \\le \\sum_{i=0}^{n-1} d_i$$$

Lean4

/-- A version of `dist_le_range_sum_dist` with each intermediate distance replaced
with an upper estimate. -/
theorem dist_le_range_sum_of_dist_le {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ}
    (hd : ∀ {k}, k < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i :=
  Nat.Ico_zero_eq_range ▸ dist_le_Ico_sum_of_dist_le (zero_le n) fun _ => hd

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