English
Let f: α → E and φ: β → α satisfy monotonicity of φ on a set t. Then the variation of the composite f ∘ φ over t is exactly the variation of f over the image φ(t): eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t).
Русский
Пусть f: α → E иφ: β → α таковы, что φ монотонно отображает t в α. Тогда вариация функции f ∘ φ на t совпадает с вариацией функции f на образе φ(t): eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t).
LaTeX
$$$eVariationOn\\bigl(f \\circ \\phi\\bigr)\\,t = eVariationOn\\!\\bigl(f\\bigr)\\bigl(\\phi''t\\bigr)$$$
Lean4
theorem comp_eq_of_monotoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) :
eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t) :=
by
apply le_antisymm (comp_le_of_monotoneOn 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 : MapsTo ψ (φ '' t) t := (surjOn_image φ t).mapsTo_invFunOn
have hψ : MonotoneOn ψ (φ '' t) := Function.monotoneOn_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_monotoneOn _ ψ hψ ψts
