Hyperbolic triangles with prescribed angles

For real numbers α, β, γ ≥ 0 with α + β + γ < π there is a convex hyperbolic triangle, with vertices in ℍ ∪ ∂ℍ, whose interior angles are α, β and γ; by ConvexPolygon.interiorAngle_eq_zero_iff, a vertex is ideal exactly when its angle is 0. Conversely, by Gauss–Bonnet, the angles of every convex hyperbolic triangle are of this form (ConvexPolygon.exists_interiorAngle_eq_iff).

The triangle is written down explicitly in one of two normal forms.

• If one angle vanishes, the corresponding vertex is ∞, and the other two vertices lie on the unit semicircle at the points of argument π - α and β (at the ideal points -1, 1 when these angles vanish). Their angles are computed by vertexAngle_infty_of_re_lt and vertexAngle_infty_of_lt_re.
• If all three angles are positive and β ≤ π / 2, the vertices are I, a point C to the right of the imaginary axis, and i e^d with cosh d = (cos α cos β + cos γ) / (sin α sin β), which exceeds 1 exactly because α + β + γ < π: this is the hyperbolic law of cosines for the side opposite C. The sides through C lie on the semicircles of centres cot α and -e^d cot β and radii 1 / sin α and e^d / sin β, whose radius vectors at C make the angle γ. The angles are computed by UpperHalfPlane.interiorAngle_of_normal_form and its companions. At most one angle of a triangle exceeds π / 2, so a cyclic relabelling puts any triangle without ideal vertices in this form.

Main results

• ConvexPolygon.triangleInfty: the convex triangle with vertices p, q and ∞, for Re p < Re q.
• ConvexPolygon.exists_interiorAngle_eq_iff: the angle triples of convex hyperbolic triangles are exactly the nonnegative triples with sum less than π.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 7 (the trigonometry of hyperbolic triangles, and the existence of a triangle with any prescribed angles of sum less than π).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Chapter 1 (hyperbolic trigonometry, including the cosine rule for angles).

A triangle with an ideal vertex at ∞

def TauCeti.UpperHalfPlane.ConvexPolygon.triangleInfty {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hlt : (toComplex p).re < (toComplex q).re) : ConvexPolygon 3

The convex triangle with vertices p, q and the ideal vertex ∞, listed counterclockwise, for points p, q ≠ ∞ of ℍ ∪ ∂ℍ with Re p < Re q.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_triangleInfty {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hp : p ≠ Sum.inr OnePoint.infty) (hq : q ≠ Sum.inr OnePoint.infty) (hlt : (toComplex p).re < (toComplex q).re) : (triangleInfty hp hq hlt).vertex = ![p, q, Sum.inr OnePoint.infty]

The vertices of ConvexPolygon.triangleInfty are p, q and ∞.

A triangle with three finite vertices

Triangles with prescribed angles

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_interiorAngle_eq_iff {α β γ : ℝ} : (∃ (P : ConvexPolygon 3), P.interiorAngle 0 = α ∧ P.interiorAngle 1 = β ∧ P.interiorAngle 2 = γ) ↔ 0 ≤ α ∧ 0 ≤ β ∧ 0 ≤ γ ∧ α + β + γ < Real.pi

Hyperbolic triangles with prescribed angles. Three real numbers are the interior angles of a convex hyperbolic triangle, with vertices in ℍ ∪ ∂ℍ, exactly when they are nonnegative with sum less than π. By ConvexPolygon.interiorAngle_eq_zero_iff, the ideal vertices of such a triangle are those with angle 0.