fixedPoint_lipschitz_in_map — Mathlib

English

If g is contracting with the same K as f, then the distance between their fixed points is bounded by the difference between f and g, scaled by (1−K)⁻¹.

Русский

Если g тоже сжатие с тем же K, то расстояние между их фиксированными точками ограничено расстоянием между f и g, умноженным на (1−K)⁻¹.

LaTeX

$$$d(p_f, p_g) \\le \\dfrac{\\sup_z d(f z, g z)}{1 - K}$, where p_f and p_g are fixed points of f and g respectively.$$

Lean4

theorem fixedPoint_lipschitz_in_map {g : α → α} (hg : ContractingWith K g) {C} (hfg : ∀ z, dist (f z) (g z) ≤ C) :
    dist (fixedPoint f hf) (fixedPoint g hg) ≤ C / (1 - K) :=
  hf.dist_fixedPoint_fixedPoint_of_dist_le' g hf.fixedPoint_isFixedPt hg.fixedPoint_isFixedPt hfg

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