English
The Euclidean distance between z and w.center(r) equals the square root of the previous expression.
Русский
Евклидово расстояние между z и w.center(r) равняется корню квадратному из соответствующего выражения.
LaTeX
$$$\\operatorname{dist}(z, w.center(r)) = \\sqrt{2\\Im(z)\\Im(w)(\\cosh(\\operatorname{dist}(z,w)) - \\cosh r) + (\\Im(w)\\sinh r)^2}.$$$
Lean4
theorem cmp_dist_eq_cmp_dist_coe_center (z w : ℍ) (r : ℝ) :
cmp (dist z w) r = cmp (dist (z : ℂ) (w.center r)) (w.im * Real.sinh r) :=
by
letI := metricSpaceAux
rcases lt_or_ge r 0 with hr₀ | hr₀
· trans Ordering.gt
exacts [(hr₀.trans_le dist_nonneg).cmp_eq_gt,
((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm]
have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity
have hzw₀ : 0 < 2 * z.im * w.im := by positivity
simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀,
← (pow_left_strictMonoOn₀ (M₀ := ℝ) two_ne_zero).cmp_map_eq dist_nonneg hr₀', dist_coe_center_sq]
rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
