Velocities of geodesic lines and the angle between two geodesics

The velocity velocity g t of the geodesic line geodesicLine g at parameter t is the derivative of t ↦ (geodesicLine g t : ℂ); it is the derivative of the Möbius map of g applied to the vertical velocity I * exp t (hasDerivAt_coe_geodesicLine, velocity_mul). The angle geodesicAngle g₁ g₂ between two geodesic lines starting at the same point is the Euclidean angle between their velocities at parameter 0. Since Möbius transformations act on velocities by multiplication by the nonzero complex number smulDeriv, the angle is invariant under the action (geodesicAngle_mul): this is the conformality of PSL(2, ℝ).

Source: Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010): the definition of the angle between geodesics as the angle between tangent vectors, §2 p. 7; Theorem 5.1 and Corollary 5.2 (Möbius transformations preserve the norm on tangent spaces, hence angles), p. 17–18.

Velocities

noncomputable def TauCeti.UpperHalfPlane.velocity (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : ℂ

The velocity of the geodesic line geodesicLine g at parameter t: the derivative of t ↦ (geodesicLine g t : ℂ), see hasDerivAt_coe_geodesicLine.

Equations

• TauCeti.UpperHalfPlane.velocity g t = g.smulDeriv (TauCeti.UpperHalfPlane.geodesicLine 1 t) * (Complex.I * ↑(Real.exp t))

theorem TauCeti.UpperHalfPlane.velocity_def (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : velocity g t = g.smulDeriv (geodesicLine 1 t) * (Complex.I * ↑(Real.exp t))

velocity is the derivative of the Möbius map applied to the vertical velocity I * exp t.

theorem TauCeti.UpperHalfPlane.hasDerivAt_coe_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : HasDerivAt (fun (s : ℝ) => ↑(geodesicLine g s)) (velocity g t) t

velocity g t is the derivative of the geodesic line geodesicLine g, as a curve in ℂ.

@[simp]

theorem TauCeti.UpperHalfPlane.velocity_ne_zero (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : velocity g t ≠ 0

Geodesic lines are regular curves: their velocity never vanishes.

@[simp]

theorem TauCeti.UpperHalfPlane.velocity_one (t : ℝ) : velocity 1 t = Complex.I * ↑(Real.exp t)

The velocity of the upward imaginary axis t ↦ i exp t.

theorem TauCeti.UpperHalfPlane.velocity_mul (h g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : velocity (h * g) t = h.smulDeriv (geodesicLine g t) * velocity g t

The chain rule: translating a geodesic line by h multiplies its velocity by the derivative of the Möbius map of h at the point.

theorem TauCeti.UpperHalfPlane.velocity_mul_pslS (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : velocity (g * pslS) t = -velocity g (-t)

Reversing a geodesic line negates its velocity.

theorem TauCeti.UpperHalfPlane.velocity_mul_dilation (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s t : ℝ) : velocity (g * ↑(Matrix.SpecialLinearGroup.dilation s)) t = velocity g (s + t)

Shifting the parameter of a geodesic line shifts its velocity.

theorem TauCeti.UpperHalfPlane.velocity_rotation (θ t : ℝ) : velocity (↑(Matrix.SpecialLinearGroup.rotation θ)) t = Complex.I * ↑(Real.exp t) / (↑(Real.cos θ) - Complex.I * ↑(Real.exp t) * ↑(Real.sin θ)) ^ 2

The velocity of the rotated imaginary axis.

theorem TauCeti.UpperHalfPlane.velocity_rotation_zero (θ : ℝ) : velocity (↑(Matrix.SpecialLinearGroup.rotation θ)) 0 = Complex.I * Complex.exp (2 * ↑θ * Complex.I)

At I, the rotation by θ turns the vertical velocity I by the angle 2θ.

The angle between two geodesic lines

noncomputable def TauCeti.UpperHalfPlane.geodesicAngle (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : ℝ

The angle between the geodesic lines of g₁ and g₂ at their common starting point geodesicLine g₁ 0 = geodesicLine g₂ 0: the Euclidean angle between their velocities.

Equations

• TauCeti.UpperHalfPlane.geodesicAngle g₁ g₂ = InnerProductGeometry.angle (TauCeti.UpperHalfPlane.velocity g₁ 0) (TauCeti.UpperHalfPlane.velocity g₂ 0)

theorem TauCeti.UpperHalfPlane.geodesicAngle_def (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle g₁ g₂ = InnerProductGeometry.angle (velocity g₁ 0) (velocity g₂ 0)

geodesicAngle is the Euclidean angle between the velocities at parameter 0.

theorem TauCeti.UpperHalfPlane.geodesicAngle_comm (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle g₁ g₂ = geodesicAngle g₂ g₁

The angle between two geodesic lines is symmetric.

theorem TauCeti.UpperHalfPlane.geodesicAngle_nonneg (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : 0 ≤ geodesicAngle g₁ g₂

Angles between geodesic lines are nonnegative.

theorem TauCeti.UpperHalfPlane.geodesicAngle_le_pi (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle g₁ g₂ ≤ Real.pi

Angles between geodesic lines are at most π.

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicAngle_self (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle g g = 0

The angle of a geodesic line with itself is 0.

theorem TauCeti.UpperHalfPlane.geodesicAngle_eq_abs_arg (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle g₁ g₂ = |(velocity g₁ 0 / velocity g₂ 0).arg|

The angle between two geodesic lines is the absolute value of the argument of the quotient of their velocities.

theorem TauCeti.UpperHalfPlane.geodesicAngle_mul (h g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (h0 : geodesicLine g₁ 0 = geodesicLine g₂ 0) : geodesicAngle (h * g₁) (h * g₂) = geodesicAngle g₁ g₂

Möbius transformations preserve angles: the angle between two geodesic lines through a common point is unchanged by translating both by h.

theorem TauCeti.UpperHalfPlane.geodesicAngle_mul_pslS_left (g₁ g₂ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicAngle (g₁ * pslS) g₂ = Real.pi - geodesicAngle g₁ g₂

Reversing the first line replaces the angle by its supplement.

theorem TauCeti.UpperHalfPlane.geodesicAngle_one_rotation {θ : ℝ} (hθ : |θ| ≤ Real.pi / 2) : geodesicAngle 1 ↑(Matrix.SpecialLinearGroup.rotation θ) = 2 * |θ|

The angle at I between the imaginary axis and its rotation by θ is 2 |θ|, for |θ| ≤ π / 2.

theorem TauCeti.UpperHalfPlane.geodesicAngle_rotation_rotation {θ φ : ℝ} (h : |θ - φ| ≤ Real.pi / 2) : geodesicAngle ↑(Matrix.SpecialLinearGroup.rotation θ) ↑(Matrix.SpecialLinearGroup.rotation φ) = 2 * |θ - φ|

The angle at I between the rotations of the imaginary axis by θ and by φ.