Angles at a vertex of ℍ ∪ ∂ℍ

The angle at a vertex p of ℍ ∪ ∂ℍ between the directions to q and r (TauCeti.UpperHalfPlane.vertexAngle p q r) is the angle between the rays UpperHalfPlane.rayToward towards q and r when p ∈ ℍ, and 0 at an ideal vertex (Walkden §7.1: geodesics meet ∂ℍ at right angles). The directional reading needs q ≠ p and r ≠ p for p ∈ ℍ: a ray towards p itself is an arbitrary geodesic line through p, so the value is then unspecified. On three points of ℍ it is UpperHalfPlane.interiorAngle (TauCeti.UpperHalfPlane.vertexAngle_inl_inl_inl).

When the vertex is a point w ∈ ℍ of the semicircle of centre m and radius ρ, the angle between the upward vertical through w and the semicircle is an arccosine of (Re w - m) / ρ; when the vertex is one of the two ideal endpoints of the semicircle the angle is 0. At a vertex where two semicircles meet with the upward vertical inside the angle, the angle is the sum of the angles to the vertical. These are the angles of a hyperbolic triangle with an ideal vertex at ∞, in the normal form of Walkden's and Katok's proofs of the Gauss–Bonnet formula.

Main declarations

• TauCeti.UpperHalfPlane.vertexAngle p q r: the angle at a vertex of ℍ ∪ ∂ℍ.
• TauCeti.UpperHalfPlane.vertexAngle_comm, TauCeti.UpperHalfPlane.vertexAngle_self, TauCeti.UpperHalfPlane.vertexAngle_nonneg, TauCeti.UpperHalfPlane.vertexAngle_le_pi, TauCeti.UpperHalfPlane.vertexAngle_smul: symmetry, vanishing, bounds and invariance.
• TauCeti.UpperHalfPlane.vertexAngle_infty_of_re_lt, TauCeti.UpperHalfPlane.vertexAngle_infty_of_lt_re: the angles at the two finite vertices of a triangle with an ideal vertex at ∞.
• TauCeti.UpperHalfPlane.vertexAngle_eq_add_of_mem_circles: an angle split by the upward vertical.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (the angle at an ideal vertex is zero) and the proof of Theorem 7.2.1 (the angles of a triangle with a vertex at ∞, with the other two vertices on a semicircle, read off as π - α and β at the endpoints of the radius vectors); Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), §5, proof of Theorem 5.4 (Figure 5.2: the angles at the two finite vertices are the angles between the radius vectors and the real axis, "as angles with mutually perpendicular sides"), and §13, proof of Siegel's theorem (the angle between consecutive sides is the sum ωₖ = βₖ + γₖ₊₁ of the angles they make with the vertical through their common vertex).

The angle at a vertex of ℍ ∪ ∂ℍ

noncomputable def TauCeti.UpperHalfPlane.vertexAngle (p q r : UpperHalfPlane ⊕ OnePoint ℝ) : ℝ

The angle at the vertex p of ℍ ∪ ∂ℍ between the directions to q and r: the angle between the rays towards q and r when p ∈ ℍ, and 0 when p is an ideal point. For p ∈ ℍ it is an angle between directions only when q ≠ p and r ≠ p; otherwise the ray towards p is an arbitrary geodesic line through p and the value is unspecified.

Equations

• TauCeti.UpperHalfPlane.vertexAngle p q r = Sum.elim (fun (A : UpperHalfPlane) => TauCeti.UpperHalfPlane.geodesicAngle (A.rayToward q) (A.rayToward r)) (fun (x : OnePoint ℝ) => 0) p

theorem TauCeti.UpperHalfPlane.vertexAngle_inl (A : UpperHalfPlane) (q r : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle (Sum.inl A) q r = geodesicAngle (A.rayToward q) (A.rayToward r)

The angle at a vertex of ℍ, unfolded.

@[simp]

theorem TauCeti.UpperHalfPlane.vertexAngle_inr (ξ : OnePoint ℝ) (q r : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle (Sum.inr ξ) q r = 0

The angle at an ideal vertex is 0.

@[simp]

theorem TauCeti.UpperHalfPlane.vertexAngle_inl_inl_inl (A B C : UpperHalfPlane) : vertexAngle (Sum.inl A) (Sum.inl B) (Sum.inl C) = A.interiorAngle B C

On three points of ℍ, the angle at a vertex is the interior angle.

theorem TauCeti.UpperHalfPlane.vertexAngle_comm (p q r : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle p r q = vertexAngle p q r

The angle at a vertex does not depend on the order of the other two points.

@[simp]

theorem TauCeti.UpperHalfPlane.vertexAngle_self (p q : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle p q q = 0

The angle at a vertex between a direction and itself is 0.

theorem TauCeti.UpperHalfPlane.vertexAngle_nonneg (p q r : UpperHalfPlane ⊕ OnePoint ℝ) : 0 ≤ vertexAngle p q r

Angles at a vertex are nonnegative.

theorem TauCeti.UpperHalfPlane.vertexAngle_le_pi (p q r : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle p q r ≤ Real.pi

Angles at a vertex are at most π.

theorem TauCeti.UpperHalfPlane.vertexAngle_inl_eq_interiorAngle (A : UpperHalfPlane) (q r : UpperHalfPlane ⊕ OnePoint ℝ) : vertexAngle (Sum.inl A) q r = A.interiorAngle (geodesicLine (A.rayToward q) 1) (geodesicLine (A.rayToward r) 1)

The angle at a vertex of ℍ towards two points of ℍ ∪ ∂ℍ is the interior angle towards the points of the two rays at parameter 1.

theorem TauCeti.UpperHalfPlane.vertexAngle_pos_of_mem_extLeftHalfPlane {A : UpperHalfPlane} {q r : UpperHalfPlane ⊕ OnePoint ℝ} (hr : r ∈ extLeftHalfPlane (A.rayToward q)) : 0 < vertexAngle (Sum.inl A) q r

The angle at a finite vertex is positive when the second target lies strictly to the left of the ray towards the first target.

theorem TauCeti.UpperHalfPlane.vertexAngle_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {p q r : UpperHalfPlane ⊕ OnePoint ℝ} (hpq : p ≠ q) (hpr : p ≠ r) : vertexAngle (h • p) (h • q) (h • r) = vertexAngle p q r

Angles at a vertex are invariant under the action.

Angles with the upward vertical

theorem TauCeti.UpperHalfPlane.vertexAngle_infty_of_re_lt {p q : UpperHalfPlane ⊕ OnePoint ℝ} {m ρ : ℝ} (hρ : 0 < ρ) (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hpm : Complex.normSq (toComplex p - ↑m) = ρ ^ 2) (hqm : Complex.normSq (toComplex q - ↑m) = ρ ^ 2) (hpq : (toComplex p).re < (toComplex q).re) : vertexAngle p (Sum.inr OnePoint.infty) q = Real.pi - Real.arccos (((toComplex p).re - m) / ρ)

The angle at the left vertex of a triangle with an ideal vertex at ∞. If p and q lie on the semicircle of centre m and radius ρ (or are among its ideal endpoints), with p to the left of q, the angle at p between the upward vertical and the direction to q is π - arccos ((Re p - m) / ρ); it is 0 when p is the ideal endpoint m - ρ.

theorem TauCeti.UpperHalfPlane.vertexAngle_infty_of_lt_re {p q : UpperHalfPlane ⊕ OnePoint ℝ} {m ρ : ℝ} (hρ : 0 < ρ) (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hpm : Complex.normSq (toComplex p - ↑m) = ρ ^ 2) (hqm : Complex.normSq (toComplex q - ↑m) = ρ ^ 2) (hpq : (toComplex p).re < (toComplex q).re) : vertexAngle q p (Sum.inr OnePoint.infty) = Real.arccos (((toComplex q).re - m) / ρ)

The angle at the right vertex of a triangle with an ideal vertex at ∞. If p and q lie on the semicircle of centre m and radius ρ (or are among its ideal endpoints), with p to the left of q, the angle at q between the direction to p and the upward vertical is arccos ((Re q - m) / ρ); it is 0 when q is the ideal endpoint m + ρ.

theorem TauCeti.UpperHalfPlane.vertexAngle_eq_add_of_mem_circles {A : UpperHalfPlane} {p q : UpperHalfPlane ⊕ OnePoint ℝ} {m₁ ρ₁ m₂ ρ₂ : ℝ} (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hA₁ : Complex.normSq (↑A - ↑m₁) = ρ₁ ^ 2) (hp₁ : Complex.normSq (toComplex p - ↑m₁) = ρ₁ ^ 2) (hA₂ : Complex.normSq (↑A - ↑m₂) = ρ₂ ^ 2) (hq₂ : Complex.normSq (toComplex q - ↑m₂) = ρ₂ ^ 2) (hpA : (toComplex p).re < A.re) (hAq : A.re < (toComplex q).re) (hp₂ : ρ₂ ^ 2 < Complex.normSq (toComplex p - ↑m₂)) : vertexAngle (Sum.inl A) p q = vertexAngle (Sum.inl A) p (Sum.inr OnePoint.infty) + vertexAngle (Sum.inl A) (Sum.inr OnePoint.infty) q

An angle split by the upward vertical. Let A ∈ ℍ lie on two semicircles, of centres m₁, m₂ and radii ρ₁, ρ₂; let p lie on the first, to the left of A, and q on the second, to the right of A (each possibly an ideal endpoint), with p strictly outside the second semicircle. Then the angle at A between the directions to p and q is the sum of the angles they make with the upward vertical through A.