comp — Mathlib

English

The composition of two AntilipschitzWith maps is Antilipschitz with the product of constants.

Русский

Состав двух антилипшитевых отображений антип Lipschitz с константами дают антилипшит

LaTeX

$$$AntilipschitzWith(K_f, f) \\land AntilipschitzWith(K_g, g) \\Rightarrow AntilipschitzWith(K_f K_g, g \\circ f)$$$

Lean4

theorem comp {Kg : ℝ≥0} {g : β → γ} (hg : AntilipschitzWith Kg g) {Kf : ℝ≥0} {f : α → β} (hf : AntilipschitzWith Kf f) :
    AntilipschitzWith (Kf * Kg) (g ∘ f) := fun x y =>
  calc
    edist x y ≤ Kf * edist (f x) (f y) := hf x y
    _ ≤ Kf * (Kg * edist (g (f x)) (g (f y))) := (mul_right_mono (hg _ _))
    _ = _ := by rw [ENNReal.coe_mul, mul_assoc]; rfl

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