English
If φ is antitone on t, the same composition invariance holds: eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t).
Русский
Если φ антинтомонна на t, то композиция сохраняет вариацию: eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t).
LaTeX
$$$eVariationOn\\bigl(f \\circ \\phi\\bigr)\\,t = eVariationOn f (\\phi''t)$$
Lean4
theorem comp_eq_of_antitoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) :
eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t) :=
by
apply le_antisymm (comp_le_of_antitoneOn f φ hφ (mapsTo_image φ t))
cases isEmpty_or_nonempty β
· convert zero_le (_ : ℝ≥0∞)
exact eVariationOn.subsingleton f <| (subsingleton_of_subsingleton.image _).anti (surjOn_image φ t)
let ψ := φ.invFunOn t
have ψφs : EqOn (φ ∘ ψ) id (φ '' t) := (surjOn_image φ t).rightInvOn_invFunOn
have ψts := (surjOn_image φ t).mapsTo_invFunOn
have hψ : AntitoneOn ψ (φ '' t) := Function.antitoneOn_of_rightInvOn_of_mapsTo hφ ψφs ψts
change eVariationOn (f ∘ id) (φ '' t) ≤ eVariationOn (f ∘ φ) t
rw [← eq_of_eqOn (ψφs.comp_left : EqOn (f ∘ φ ∘ ψ) (f ∘ id) (φ '' t))]
exact comp_le_of_antitoneOn _ ψ hψ ψts
