English
A version of the Ico-sum distance bound where each intermediate distance is bounded by a given d_k, giving dist(f(m), f(n)) ≤ sum d_k over k in Ico m n.
Русский
Версия границы суммы расстояний по Ico, когда каждое промежуточное расстояние ограничено d_k: dist(f(m), f(n)) ≤ сумма d_k по k в Ico m n.
LaTeX
$$$\\forall m \\le n, \\mathrm{dist}(f(m), f(n)) \\le \\sum_{i=m}^{n-1} d_i \\quad\\text{при условии}\\quad \\mathrm{dist}(f(k), f(k+1)) \\le d_k$$$
Lean4
/-- A version of `dist_le_Ico_sum_dist` with each intermediate distance replaced
with an upper estimate. -/
theorem dist_le_Ico_sum_of_dist_le {f : ℕ → α} {m n} (hmn : m ≤ n) {d : ℕ → ℝ}
(hd : ∀ {k}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i :=
le_trans (dist_le_Ico_sum_dist f hmn) <|
Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2
