Real translations of the upper half-plane

A real number r translates a point z of ℍ to r +ᵥ z. The translation is an isometry of the hyperbolic metric but not of the modulus: for r ≠ 0 it preserves ‖z‖ exactly when z lies on the perpendicular bisector re = -r / 2 of 0 and -r, since then z and r +ᵥ z are mirror images in the imaginary axis. The lemmas here prove that this condition is sufficient, for every r. For r = ±1 that line contains a vertical edge of the standard fundamental domain, which is how the fundamental-domain API uses these lemmas.

Main results

• UpperHalfPlane.normSq_coe_vadd_of_re_eq, UpperHalfPlane.norm_coe_vadd_of_re_eq: on the line re = -r / 2, translation by r preserves the squared norm and the norm.

theorem UpperHalfPlane.normSq_coe_vadd_of_re_eq {r : ℝ} {p : UpperHalfPlane} (hre : p.re = -r / 2) : Complex.normSq ↑(r +ᵥ p) = Complex.normSq ↑p

On the perpendicular bisector re = -r / 2 of 0 and -r, translation by r preserves the norm-square.

theorem UpperHalfPlane.norm_coe_vadd_of_re_eq {r : ℝ} {p : UpperHalfPlane} (hre : p.re = -r / 2) : ‖↑(r +ᵥ p)‖ = ‖↑p‖

On the line re = -r / 2, translation by r preserves the norm.