English
The composition of Lipschitz functions is Lipschitz: if f is Kf-Lipschitz and g is Kg-Lipschitz, then f ∘ g is (Kf Kg)‑Lipschitz.
Русский
Сочетание липшицевых отображений сохраняет липшицевость: если f липшицево с константой Kf и g липшицево с Kg, то f∘g липшицево с константой KfKg.
LaTeX
$$$\\text{LipschitzWith } K_f f \\to \\text{ LipschitzWith } K_g g \\Rightarrow \\text{ LipschitzWith } (K_f K_g) (f \\circ g)$$$
Lean4
/-- The composition of Lipschitz functions is Lipschitz. -/
protected theorem comp {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf * Kg) (f ∘ g) := fun x y =>
calc
edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) := hf _ _
_ ≤ Kf * (Kg * edist x y) := (mul_right_mono (hg _ _))
_ = (Kf * Kg : ℝ≥0) * edist x y := by rw [← mul_assoc, ENNReal.coe_mul]
