English
If φ is monotone on t and maps t into s, then the variation of f∘φ on t is bounded by the variation of f on s.
Русский
Если φ монотонно отображает t в s и т.д., вариация f∘φ на t не превосходит вариацию f на s.
LaTeX
$$$\forall f:α\to E,\; {s,t:\ Set α},\; φ:β\to α,\; MonotoneOn φ t\;\Rightarrow\; MapsTo φ t s\;\Rightarrow eVariationOn (f\circ φ) t \le eVariationOn f s$$
Lean4
theorem sum' (f : α → E) {I : ℕ → α} (hI : Monotone I) {n : ℕ} :
∑ i ∈ Finset.range n, eVariationOn f (Icc (I i) (I (i + 1))) = eVariationOn f (Icc (I 0) (I n)) :=
by
convert
sum f hI (s := Icc (I 0) (I n)) (n := n) (hn := by intros; rw [mem_Icc]; constructor <;> (apply hI; omega)) with i
hi
· simp only [right_eq_inter]
gcongr <;> (apply hI; rw [Finset.mem_range] at hi; omega)
· simp
