English
A general upper bound for edist along a finite Ico segment using arbitrary upper bounds d(i) for each step.
Русский
Обобщённое верхнее ограничение edist вдоль конечного сегмента Ico с заданными верхними гранками d(i) для каждого шага.
LaTeX
$$$\forall f:\mathbb{N} \to \alpha, {m,n},\; (m\le n)\Rightarrow edist(f(m), f(n)) \le \sum_{i=m}^{n-1} d(i) \,\text{provided each } edist(f(i), f(i+1)) \le d(i).$$$
Lean4
/-- A version of `edist_le_Ico_sum_edist` with each intermediate distance replaced
with an upper estimate. -/
theorem edist_le_Ico_sum_of_edist_le {f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ≥0∞}
(hd : ∀ {k}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i :=
le_trans (edist_le_Ico_sum_edist f hmn) <|
Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2
