English
If hf is AntilipschitzWith Kf f and hg is LipschitzWith Kg g, with hK: Kg < Kf⁻¹, then the product map is antilipschitz with constant (Kf⁻¹ - Kg)⁻¹ scaled by g.
Русский
Если f — антилипшиц с константой Kf, а g — липшиц с Kg и Kg < Kf⁻¹, то произведение f·g является антилипшицевым с константой (Kf⁻¹ - Kg)⁻¹, умноженным на g.
LaTeX
$$$\\mathrm{AntilipschitzWith}\\ K_f\\ f\\;\\rightarrow\\; \\mathrm{LipschitzWith}\\ K_g\\ g\\Rightarrow \\mathrm{AntilipschitzWith}\\ (K_f^{-1}-K_g)^{-1}\\; (\\lambda x. f(x)g(x)).$$$
Lean4
@[to_additive]
theorem mul_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) :
AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x :=
by
letI : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace hf.edist_ne_top
refine AntilipschitzWith.of_le_mul_dist fun x y => ?_
rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]
rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]
rw [mul_comm, NNReal.coe_sub hK.le, sub_mul]
calc
↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
_ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)
