Elliptic and cusp parameters for hyperbolic triangles

A vertex of a finite-area hyperbolic triangle is either elliptic, with a finite order m ≥ 2, or ideal, in which case it is a cusp. TriangleOrder keeps those alternatives distinct instead of encoding a cusp by an untyped infinity value. Its reciprocal contribution is 1 / m at an elliptic vertex and 0 at a cusp; multiplying by π gives the corresponding interior angle.

The predicate TriangleOrder.IsHyperbolic p q r is the typed hyperbolic triangle inequality p.reciprocal + q.reciprocal + r.reciprocal < 1. The main comparison theorem rewrites it as the geometric angle inequality p.angle + q.angle + r.angle < π.

Main declarations

• TriangleOrder: an elliptic order m ≥ 2 or a cusp.
• TriangleOrder.reciprocal: the contribution 1 / m or 0 to the triangle inequality.
• TriangleOrder.angle: the corresponding angle π / m or 0.
• TriangleOrder.IsHyperbolic: the typed reciprocal-sum condition for a hyperbolic triple.

References

S. Katok, Fuchsian Groups, Chicago Lectures in Mathematics (1992), §3.1.

inductive TauCeti.TriangleOrder : Type

The order attached to a vertex of a finite-area hyperbolic triangle: either a finite elliptic order m ≥ 2, or a cusp.

• elliptic (m : ℕ) (hm : 2 ≤ m) : TriangleOrder

  An elliptic vertex of order m ≥ 2.

• cusp : TriangleOrder

  An ideal vertex, with angle zero.

def TauCeti.instDecidableEqTriangleOrder.decEq (x✝ x✝¹ : TriangleOrder) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.instDecidableEqTriangleOrder.decEq (TauCeti.TriangleOrder.elliptic m hm) TauCeti.TriangleOrder.cusp = isFalse ⋯
• TauCeti.instDecidableEqTriangleOrder.decEq TauCeti.TriangleOrder.cusp (TauCeti.TriangleOrder.elliptic m hm) = isFalse ⋯
• TauCeti.instDecidableEqTriangleOrder.decEq TauCeti.TriangleOrder.cusp TauCeti.TriangleOrder.cusp = isTrue ⋯

@[instance_reducible]

instance TauCeti.instDecidableEqTriangleOrder : DecidableEq TriangleOrder

Equations

• TauCeti.instDecidableEqTriangleOrder = TauCeti.instDecidableEqTriangleOrder.decEq

noncomputable def TauCeti.TriangleOrder.reciprocal : TriangleOrder → ℝ

The reciprocal contribution of a triangle vertex: 1 / m for an elliptic vertex of order m, and 0 for a cusp.

Equations

• (TauCeti.TriangleOrder.elliptic m hm).reciprocal = (↑m)⁻¹
• TauCeti.TriangleOrder.cusp.reciprocal = 0

@[simp]

theorem TauCeti.TriangleOrder.reciprocal_elliptic (m : ℕ) (hm : 2 ≤ m) : (elliptic m hm).reciprocal = (↑m)⁻¹

The reciprocal contribution of an elliptic vertex is the inverse of its order.

@[simp]

theorem TauCeti.TriangleOrder.reciprocal_cusp : cusp.reciprocal = 0

A cusp contributes zero to the reciprocal sum.

theorem TauCeti.TriangleOrder.reciprocal_nonneg (p : TriangleOrder) : 0 ≤ p.reciprocal

Reciprocal contributions are nonnegative.

@[simp]

theorem TauCeti.TriangleOrder.reciprocal_pos_iff (p : TriangleOrder) : 0 < p.reciprocal ↔ p ≠ cusp

The reciprocal contribution is positive exactly at an elliptic vertex.

@[simp]

theorem TauCeti.TriangleOrder.reciprocal_eq_zero_iff (p : TriangleOrder) : p.reciprocal = 0 ↔ p = cusp

The reciprocal contribution vanishes exactly at a cusp.

theorem TauCeti.TriangleOrder.reciprocal_lt_one (p : TriangleOrder) : p.reciprocal < 1

Every triangle-order reciprocal is strictly less than one.

theorem TauCeti.TriangleOrder.reciprocal_le_half (p : TriangleOrder) : p.reciprocal ≤ 2⁻¹

Every triangle-order reciprocal is at most 1 / 2; equality is attained only at elliptic order two.

@[simp]

theorem TauCeti.TriangleOrder.reciprocal_eq_inv_two_iff (p : TriangleOrder) : p.reciprocal = 2⁻¹ ↔ p = elliptic 2 reciprocal_eq_inv_two_iff._proof_1

Reciprocal contribution is 1 / 2 exactly at an elliptic vertex of order two.

theorem TauCeti.TriangleOrder.reciprocal_injective : Function.Injective reciprocal

Reciprocal contribution distinguishes triangle orders.

noncomputable def TauCeti.TriangleOrder.angle (p : TriangleOrder) : ℝ

The interior angle attached to a triangle vertex: π / m at an elliptic vertex of order m, and 0 at a cusp.

Equations

• p.angle = Real.pi * p.reciprocal

theorem TauCeti.TriangleOrder.angle_def (p : TriangleOrder) : p.angle = Real.pi * p.reciprocal

A triangle-order angle is π times its reciprocal contribution.

@[simp]

theorem TauCeti.TriangleOrder.angle_elliptic (m : ℕ) (hm : 2 ≤ m) : (elliptic m hm).angle = Real.pi / ↑m

The angle at an elliptic vertex of order m is π / m.

@[simp]

theorem TauCeti.TriangleOrder.angle_cusp : cusp.angle = 0

The angle at a cusp is zero.

theorem TauCeti.TriangleOrder.angle_nonneg (p : TriangleOrder) : 0 ≤ p.angle

Triangle-order angles are nonnegative.

@[simp]

theorem TauCeti.TriangleOrder.angle_pos_iff (p : TriangleOrder) : 0 < p.angle ↔ p ≠ cusp

A triangle-order angle is positive exactly at an elliptic vertex.

@[simp]

theorem TauCeti.TriangleOrder.angle_eq_zero_iff (p : TriangleOrder) : p.angle = 0 ↔ p = cusp

A triangle-order angle vanishes exactly at a cusp.

theorem TauCeti.TriangleOrder.angle_le_pi_div_two (p : TriangleOrder) : p.angle ≤ Real.pi / 2

Every triangle-order angle is at most π / 2.

theorem TauCeti.TriangleOrder.angle_lt_pi (p : TriangleOrder) : p.angle < Real.pi

Every triangle-order angle is strictly less than π.

def TauCeti.TriangleOrder.IsHyperbolic (p q r : TriangleOrder) : Prop

The typed hyperbolic triangle condition: the sum of the three reciprocal contributions is strictly less than one.

Equations

• p.IsHyperbolic q r = (p.reciprocal + q.reciprocal + r.reciprocal < 1)

theorem TauCeti.TriangleOrder.isHyperbolic_iff (p q r : TriangleOrder) : p.IsHyperbolic q r ↔ p.reciprocal + q.reciprocal + r.reciprocal < 1

The typed hyperbolic condition, unfolded as the reciprocal-sum inequality.

theorem TauCeti.TriangleOrder.IsHyperbolic.swap {p q r : TriangleOrder} (h : p.IsHyperbolic q r) : q.IsHyperbolic p r

The hyperbolic condition is unchanged by swapping the first two vertices.

theorem TauCeti.TriangleOrder.IsHyperbolic.rotate {p q r : TriangleOrder} (h : p.IsHyperbolic q r) : q.IsHyperbolic r p

The hyperbolic condition is unchanged by cyclically rotating the vertices.

@[simp]

theorem TauCeti.TriangleOrder.isHyperbolic_cusp_cusp_cusp : cusp.IsHyperbolic cusp cusp

Three cusps satisfy the typed hyperbolic triangle condition.

theorem TauCeti.TriangleOrder.isHyperbolic_iff_angle_sum_lt_pi (p q r : TriangleOrder) : p.IsHyperbolic q r ↔ p.angle + q.angle + r.angle < Real.pi

The reciprocal and angle forms of the hyperbolic triangle condition agree.