The geodesic through two points as a semicircle

This file makes the classical description of the geodesics of ℍ quantitative, for the geodesic geodesicBetween P Q from P to Q. The affine map UpperHalfPlane.toPoint P : z ↦ P.im * z + P.re sends I to P, so geodesicBetween P Q is toPoint P followed by a rotation of the imaginary axis (exists_geodesicBetween_eq_toPoint_mul_rotation); the half-planes of a rotated axis are given by an explicit quadratic form (mem_rightHalfPlane_rotation_iff).

When P.re ≠ Q.re, the geodesic through P and Q is the semicircle centred at UpperHalfPlane.circleCenter P Q on the real axis, which passes through both points (UpperHalfPlane.normSq_sub_circleCenter, mem_range_geodesicLine_geodesicBetween_iff_of_re_ne), and it is the only such point of the real axis (UpperHalfPlane.circleCenter_eq_of_normSq_eq); its right half-plane is the inside of that disc when Q is to the right of P and the outside when Q is to the left (mem_rightHalfPlane_geodesicBetween_iff_of_re_lt, mem_rightHalfPlane_geodesicBetween_iff_of_lt_re), and its velocity at P is tangent to the semicircle, oriented clockwise exactly when Q is to the right of P (exists_velocity_geodesicBetween_zero_eq). When P.re = Q.re the geodesic is the vertical line through P (geodesicBetween_eq_toPoint_of_re_eq, mem_rightHalfPlane_geodesicBetween_iff_of_re_eq, exists_velocity_geodesicBetween_zero_eq_of_re_eq). Conversely, a geodesic line running between two points (other than ∞) of a circle centred on the real axis, with distinct real parts, lies on that circle (IsGeodesicFromTo.normSq_geodesicLine_sub).

Source: Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), §3 Theorem 3.1 (p. 10): the geodesics in ℍ are the semicircles and the rays orthogonal to the real axis.

The half-planes of a rotated axis, explicitly

theorem TauCeti.UpperHalfPlane.re_rotation_inv_smul (θ : ℝ) (w : UpperHalfPlane) : ((↑(Matrix.SpecialLinearGroup.rotation θ))⁻¹ • w).re = (Real.sin θ * Real.cos θ * (Complex.normSq ↑w - 1) + (Real.cos θ ^ 2 - Real.sin θ ^ 2) * w.re) / Complex.normSq (↑(Real.sin θ) * ↑w + ↑(Real.cos θ))

The real part after the inverse rotation by θ, as a quadratic form in the point: the numerator vanishes exactly on the rotated imaginary axis.

theorem TauCeti.UpperHalfPlane.normSq_sin_mul_add_cos_pos (θ : ℝ) (w : UpperHalfPlane) : 0 < Complex.normSq (↑(Real.sin θ) * ↑w + ↑(Real.cos θ))

The denominator of re_rotation_inv_smul is positive.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_rotation_iff (θ : ℝ) (w : UpperHalfPlane) : w ∈ rightHalfPlane ↑(Matrix.SpecialLinearGroup.rotation θ) ↔ 0 < Real.sin θ * Real.cos θ * (Complex.normSq ↑w - 1) + (Real.cos θ ^ 2 - Real.sin θ ^ 2) * w.re

Membership in the right half-plane of a rotated axis, as a quadratic inequality.

theorem TauCeti.UpperHalfPlane.re_rotation_smul_mk (θ y : ℝ) (hy : 0 < y) : (Matrix.SpecialLinearGroup.rotation θ • { coe := { re := 0, im := y }, coe_im_pos := hy }).re = Real.sin θ * Real.cos θ * (1 - y ^ 2) / Complex.normSq (↑(Real.cos θ) - Complex.I * ↑y * ↑(Real.sin θ))

The real part of a point of the rotated axis, at height y before rotating.

The centre of the semicircle through two points

theorem UpperHalfPlane.abs_re_sub_lt_sqrt_normSq (P : UpperHalfPlane) (c : ℝ) : |P.re - c| < √(Complex.normSq (↑P - ↑c))

A point of ℍ lies strictly between the two ends of any semicircle through it: its real part is within less than the radius |P - c| of the centre c.

noncomputable def UpperHalfPlane.circleCenter (P Q : UpperHalfPlane) : ℝ

The centre on the real axis of the semicircle through P and Q, when P.re ≠ Q.re.

Equations

• P.circleCenter Q = (Complex.normSq ↑Q - Complex.normSq ↑P) / (2 * (Q.re - P.re))

theorem UpperHalfPlane.circleCenter_def (P Q : UpperHalfPlane) : P.circleCenter Q = (Complex.normSq ↑Q - Complex.normSq ↑P) / (2 * (Q.re - P.re))

The centre of the semicircle through P and Q, as a formula.

theorem UpperHalfPlane.circleCenter_comm (P Q : UpperHalfPlane) : Q.circleCenter P = P.circleCenter Q

The centre of the semicircle through two points does not depend on their order.

theorem UpperHalfPlane.normSq_sub_circleCenter {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) : Complex.normSq (↑Q - ↑(P.circleCenter Q)) = Complex.normSq (↑P - ↑(P.circleCenter Q))

Both endpoints lie on the semicircle: they are equidistant from its centre.

theorem UpperHalfPlane.circleCenter_eq_of_normSq_eq {P Q : UpperHalfPlane} {m : ℝ} (hPQ : P.re ≠ Q.re) (h : Complex.normSq (↑P - ↑m) = Complex.normSq (↑Q - ↑m)) : P.circleCenter Q = m

A point m of the real axis equidistant from P and Q, with P.re ≠ Q.re, is the centre of the semicircle through P and Q.

The geodesic through two points as a semicircle

theorem TauCeti.UpperHalfPlane.exists_geodesicBetween_eq_toPoint_mul_rotation {P Q : UpperHalfPlane} (hPQ : P ≠ Q) : ∃ (θ : ℝ), geodesicBetween P Q = P.toPoint * ↑(Matrix.SpecialLinearGroup.rotation θ) ∧ UpperHalfPlane.I ≠ P.toPoint⁻¹ • Q ∧ geodesicBetween UpperHalfPlane.I (P.toPoint⁻¹ • Q) = ↑(Matrix.SpecialLinearGroup.rotation θ)

The geodesic from P to Q is the normalising map of P followed by a rotation of the imaginary axis.

theorem TauCeti.UpperHalfPlane.exists_rotation_of_re_ne {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) : ∃ (θ : ℝ), geodesicBetween P Q = P.toPoint * ↑(Matrix.SpecialLinearGroup.rotation θ) ∧ 0 < Real.sin θ * Real.cos θ * (P.re - Q.re) ∧ P.circleCenter Q = P.re - (Real.cos θ ^ 2 - Real.sin θ ^ 2) * P.im / (2 * (Real.sin θ * Real.cos θ))

The semicircle case: the geodesic from P to Q is toPoint P followed by a rotation by an angle θ, whose sign is opposite to that of Q.re - P.re, and the centre of the semicircle through P and Q is P.re - cos 2θ / sin 2θ · P.im.

theorem TauCeti.UpperHalfPlane.exists_re_inv_geodesicBetween_smul_eq {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) (z : UpperHalfPlane) : ∃ (κ : ℝ), 0 < κ ∧ ((geodesicBetween P Q)⁻¹ • z).re = κ * ((P.re - Q.re) * (Complex.normSq (↑z - ↑(P.circleCenter Q)) - Complex.normSq (↑P - ↑(P.circleCenter Q))))

The semicircle case: after applying the inverse of the geodesic from P to Q, the real part of a point is a positive multiple of (P.re - Q.re) · (|z - c|² - |P - c|²), where c is the centre of the semicircle through P and Q.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_geodesicBetween_iff_of_re_ne {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) (z : UpperHalfPlane) : z ∈ rightHalfPlane (geodesicBetween P Q) ↔ 0 < (P.re - Q.re) * (Complex.normSq (↑z - ↑(P.circleCenter Q)) - Complex.normSq (↑P - ↑(P.circleCenter Q)))

The semicircle case of the description of the half-planes of geodesicBetween P Q: the right half-plane is the inside of the disc through P and Q centred on the real axis when Q is to the right of P, and the outside when it is to the left.

theorem TauCeti.UpperHalfPlane.mem_leftHalfPlane_geodesicBetween_iff_of_re_ne {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) (z : UpperHalfPlane) : z ∈ leftHalfPlane (geodesicBetween P Q) ↔ (P.re - Q.re) * (Complex.normSq (↑z - ↑(P.circleCenter Q)) - Complex.normSq (↑P - ↑(P.circleCenter Q))) < 0

The left half-plane of the geodesic from P to Q, in the semicircle case.

theorem TauCeti.UpperHalfPlane.mem_range_geodesicLine_geodesicBetween_iff_of_re_ne {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) (z : UpperHalfPlane) : z ∈ Set.range (geodesicLine (geodesicBetween P Q)) ↔ Complex.normSq (↑z - ↑(P.circleCenter Q)) = Complex.normSq (↑P - ↑(P.circleCenter Q))

The geodesic through P and Q, as a set, is the semicircle through them centred on the real axis.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_geodesicBetween_iff_of_re_lt {P Q : UpperHalfPlane} (hPQ : P.re < Q.re) (z : UpperHalfPlane) : z ∈ rightHalfPlane (geodesicBetween P Q) ↔ Complex.normSq (↑z - ↑(P.circleCenter Q)) < Complex.normSq (↑P - ↑(P.circleCenter Q))

The geodesic from P to a point Q to its right runs clockwise along the semicircle through them, so its right half-plane is the inside of the disc.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_geodesicBetween_iff_of_lt_re {P Q : UpperHalfPlane} (hPQ : Q.re < P.re) (z : UpperHalfPlane) : z ∈ rightHalfPlane (geodesicBetween P Q) ↔ Complex.normSq (↑P - ↑(P.circleCenter Q)) < Complex.normSq (↑z - ↑(P.circleCenter Q))

The geodesic from P to a point Q to its left runs counterclockwise along the semicircle through them, so its right half-plane is the outside of the disc.

theorem TauCeti.UpperHalfPlane.geodesicBetween_eq_toPoint_of_re_eq {P Q : UpperHalfPlane} (h : P.re = Q.re) (hPQ : P.im < Q.im) : geodesicBetween P Q = P.toPoint

The geodesic from P up to a point Q above it is the vertical line through P.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_geodesicBetween_iff_of_re_eq {P Q : UpperHalfPlane} (h : P.re = Q.re) (hPQ : P.im < Q.im) (z : UpperHalfPlane) : z ∈ rightHalfPlane (geodesicBetween P Q) ↔ P.re < z.re

The geodesic from P up to a point Q above it is a vertical line; its right half-plane is the side of larger real part.

theorem TauCeti.UpperHalfPlane.exists_velocity_geodesicBetween_zero_eq {P Q : UpperHalfPlane} (hPQ : P.re ≠ Q.re) : ∃ (μ : ℝ), μ * (Q.re - P.re) < 0 ∧ velocity (geodesicBetween P Q) 0 = ↑μ * (Complex.I * (↑P - ↑(P.circleCenter Q)))

The velocity at P of the geodesic from P to Q is tangent to the semicircle through them, with the clockwise orientation exactly when Q is to the right of P.

theorem TauCeti.UpperHalfPlane.exists_velocity_geodesicBetween_zero_eq_of_re_eq {P Q : UpperHalfPlane} (h : P.re = Q.re) (hPQ : P ≠ Q) : ∃ (μ : ℝ), 0 < μ ∧ velocity (geodesicBetween P Q) 0 = ↑μ * (↑Q.im - ↑P.im) * Complex.I

The velocity at P of the vertical geodesic from P to Q points up exactly when Q is above P.

Geodesic lines through two points of a semicircle

theorem TauCeti.UpperHalfPlane.IsGeodesicFromTo.normSq_geodesicLine_sub {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} {m r : ℝ} (hg : IsGeodesicFromTo g p q) (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hpm : Complex.normSq (toComplex p - ↑m) = r) (hqm : Complex.normSq (toComplex q - ↑m) = r) (hre : (toComplex p).re ≠ (toComplex q).re) (t : ℝ) : Complex.normSq (↑(geodesicLine g t) - ↑m) = r

A geodesic line running between two points (other than ∞) of a circle centred on the real axis, with distinct real parts, lies on that circle.