English
If f and g are LipschitzOnWith on a set s with constants Kf and Kg, then the product x ↦ f(x) g(x) is LipschitzOnWith with constant Kf+Kg on s.
Русский
Если f и g липшицевы на s с константами Kf и Kg, то произведение x↦f(x)g(x) липшицево на s с константой Kf+Kg.
LaTeX
$$$\\mathrm{LipschitzOnWith}\\ K_f f\\ s \\land \\mathrm{LipschitzOnWith}\\ Kg\\ g\\ s \\Rightarrow \\mathrm{LipschitzOnWith}\\ (K_f+K_g)\\ (\\lambda x. f(x)g(x))\\ s$$$
Lean4
@[to_additive]
theorem mul (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf + Kg) (fun x ↦ f x * g x) s := fun x hx y hy ↦
calc
edist (f x * g x) (f y * g y) ≤ edist (f x) (f y) + edist (g x) (g y) := edist_mul_mul_le _ _ _ _
_ ≤ Kf * edist x y + Kg * edist x y := (add_le_add (hf hx hy) (hg hx hy))
_ = (Kf + Kg) * edist x y := (add_mul _ _ _).symm
