English
For a,b,c in the upper half-plane, sinh of half the sum of two consecutive distances equals a rational expression involving distances to conjugates and imaginary parts.
Русский
Для a,b,c в верхней полуплоскости, sinh половины суммы двух соседних расстояний равен рациональному выражению, зависящему от расстояний до сопряжённых и мнимой частей.
LaTeX
$$$\sinh\left(\frac{\mathrm{dist}(a,b) + \mathrm{dist}(b,c)}{2}\right) = \frac{\mathrm{dist}(a,b) \mathrm{dist}(c,\overline{b}) + \mathrm{dist}(b,c) \mathrm{dist}(a,\overline{b})}{2 \sqrt{a.im \cdot c.im} \; \mathrm{dist}(b, \overline{b})}$$$
Lean4
theorem sinh_half_dist_add_dist (a b c : ℍ) :
sinh ((dist a b + dist b c) / 2) =
(dist (a : ℂ) b * dist (c : ℂ) (conj ↑b) + dist (b : ℂ) c * dist (a : ℂ) (conj ↑b)) /
(2 * √(a.im * c.im) * dist (b : ℂ) (conj ↑b)) :=
by
simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]
rw [← add_div, Complex.dist_self_conj, coe_im, abs_of_pos b.im_pos, mul_comm (dist (b : ℂ) _), dist_comm (b : ℂ),
Complex.dist_conj_comm, mul_mul_mul_comm, mul_mul_mul_comm _ _ _ b.im]
congr 2
rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt, mul_comm] <;> exact (im_pos _).le
