English
If u is monotone on the closed interval Icc m n and maps into s, then the sum of edists along the chain covers at most eVariationOn f s.
Русский
Если u монотонна на отрезке Icc(m,n) и принимает значения в s, то сумма edist вдоль цепи не превосходит eVariationOn f s.
LaTeX
$$$\forall f:α\to E,\;\forall s,\forall m,n\in\mathbb{N},\; u:\mathbb{N}\to α \\; (\text{MonotoneOn }u(Icc(m,n))) \\; (\forall i\in Icc(m,n), u(i)\in s) \\Rightarrow \sum_{i\in Finset.Ico\,m\,n} edist(f(u(i+1)), f(u(i))) \le eVariationOn f s$$
Lean4
theorem sum_le_of_monotoneOn_Icc (f : α → E) {s : Set α} {m n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Icc m n))
(us : ∀ i ∈ Icc m n, u i ∈ s) : (∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i))) ≤ eVariationOn f s :=
by
rcases le_total n m with hnm | hmn
· simp [Finset.Ico_eq_empty_of_le hnm]
let π := projIcc m n hmn
let v i := u (π i)
calc
∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) = ∑ i ∈ Finset.Ico m n, edist (f (v (i + 1))) (f (v i)) :=
Finset.sum_congr rfl fun i hi ↦ by
rw [Finset.mem_Ico] at hi
simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩, projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]
_ ≤ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) :=
(Finset.sum_mono_set _ (Nat.Iio_eq_range ▸ Finset.Ico_subset_Iio_self))
_ ≤ eVariationOn f s := sum_le _ _ (fun i j h ↦ hu (π i).2 (π j).2 (monotone_projIcc hmn h)) fun i ↦ us _ (π i).2
