English
If φ is antitone on t and maps t into s, then composing f with φ does not increase the variation: eVariationOn (f ∘ φ) t ≤ eVariationOn f s.
Русский
Если φ антимонотонна на t и отображает t в s, то композиция f ∘ φ не увеличивает eVariationOn: eVariationOn (f ∘ φ) t ≤ eVariationOn f s.
LaTeX
$$$ eVariationOn (f \circ \varphi) t \le eVariationOn f s $$$
Lean4
theorem comp_le_of_antitoneOn (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t)
(φst : MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s :=
by
refine iSup_le ?_
rintro ⟨n, u, hu, ut⟩
rw [← Finset.sum_range_reflect]
refine
(Finset.sum_congr rfl fun x hx => ?_).trans_le <|
le_iSup_of_le
⟨n, fun i => φ (u <| n - i), fun x y xy => hφ (ut _) (ut _) (hu <| Nat.sub_le_sub_left xy n), fun i =>
φst (ut _)⟩
le_rfl
rw [Finset.mem_range] at hx
dsimp only [Subtype.coe_mk, Function.comp_apply]
rw [edist_comm]
congr 4 <;> omega
