English
The squared Euclidean distance between z and w.center(r) equals 2·Im(z)·Im(w)·(cosh(dist(z,w)) − cosh(r)) + (Im(w)·sinh(r))^2.
Русский
Квадрат евклидова расстояния между z и w.center(r) равно 2·Im(z)·Im(w)·(cosh(dist(z,w)) − cosh(r)) + (Im(w)·sinh(r))^2.
LaTeX
$$$\\operatorname{dist}(z, w.center(r))^2 = 2 \\operatorname{Im}(z) \\operatorname{Im}(w) (\\cosh(\\operatorname{dist}(z,w)) - \\cosh r) + (\\operatorname{Im}(w) \\sinh r)^2.$$$
Lean4
theorem dist_coe_center_sq (z w : ℍ) (r : ℝ) :
dist (z : ℂ) (w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2 :=
by
have H : 2 * z.im * w.im ≠ 0 := by positivity
simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im, cosh_dist',
mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ← sq]
ring
