English
If f is contracting with K, then for all x,y with edist(x,y) finite, the edistance satisfies an inequality relating distances to f(x), f(y) and edist(x,y) itself: edist x y ≤ (edist x f x + edist y f y) / (1 - K).
Русский
Если f сжимающий с коэффициентом K, то для всех x,y с конечной edist x y выполняется неравенство, связывающее расстояния до f(x), f(y) и edist(x,y): edist x y ≤ (edist x f x + edist y f y) / (1 - K).
LaTeX
$$$\mathrm{edist}(x,y) \le \dfrac{\mathrm{edist}(x,f(x)) + \mathrm{edist}(y,f(y))}{1- K}.$$$
Lean4
theorem edist_inequality (hf : ContractingWith K f) {x y} (h : edist x y ≠ ∞) :
edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - K) :=
suffices edist x y ≤ edist x (f x) + edist y (f y) + K * edist x y by
rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top), mul_comm,
ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
calc
edist x y ≤ edist x (f x) + edist (f x) (f y) + edist (f y) y := edist_triangle4 _ _ _ _
_ = edist x (f x) + edist y (f y) + edist (f x) (f y) := by rw [edist_comm y, add_right_comm]
_ ≤ edist x (f x) + edist y (f y) + K * edist x y := add_le_add le_rfl (hf.2 _ _)
