mul_div_lipschitzWith — Mathlib

English

If hf is AntilipschitzWith Kf f and hg is LipschitzWith Kg (g/f) with hK: Kg < Kf⁻¹, then the divisor product map is antilipschitz with a computed constant.

Русский

Если hf — антилипшицево с константой Kf для f, а hg — липшицев с Kg для (g/f) и Kg < Kf⁻¹, то отображение (g/f) упорядочивает антилипшицевость с рассчитанной константой.

LaTeX

$$$\\mathrm{AntilipschitzWith}\\ K_f\\ f \\land \\mathrm{LipschitzWith}\\ Kg\\left(\\frac{g}{f}\\right) \\Rightarrow \\mathrm{AntilipschitzWith}\\ (K_f^{-1}-K_g)^{-1}\\; g.$$$

Lean4

@[to_additive]
theorem mul_div_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) :
    AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g := by simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK

Похожие утверждения