English
The complex distance between z and w is bounded by the Euclidean distance to the center via a simple inequality.
Русский
Гиперболическая дистанция ограничена евклидовым расстоянием через центр: d_ℂ(z,w) ≤ …
LaTeX
$$$\\operatorname{dist}_{\\mathbb{C}}(z,w) \\le \\operatorname{Im}(w) \\Bigl( e^{\\operatorname{dist}(z,w)} - 1 \\Bigr).$$$
Lean4
/-- An upper estimate on the complex distance between two points in terms of the hyperbolic distance
and the imaginary part of one of the points. -/
theorem dist_coe_le (z w : ℍ) : dist (z : ℂ) w ≤ w.im * (Real.exp (dist z w) - 1) :=
calc
dist (z : ℂ) w ≤ dist (z : ℂ) (w.center (dist z w)) + dist (w : ℂ) (w.center (dist z w)) :=
dist_triangle_right _ _ _
_ = w.im * (Real.exp (dist z w) - 1) := by
rw [dist_center_dist, dist_self_center, ← mul_add, ← add_sub_assoc, Real.sinh_add_cosh]
