The Gauss–Bonnet formula for convex hyperbolic polygons with ideal vertices

The invariant area of a convex hyperbolic polygon with n vertices in ℍ ∪ ∂ℍ and interior angles α₀, …, αₙ₋₁ (with αᵢ = 0 at an ideal vertex) is (n - 2) π - (α₀ + ⋯ + αₙ₋₁) (ConvexPolygon.volume_carrier). In particular the area is finite (ConvexPolygon.volume_carrier_ne_top), the angle sum is at most (n - 2) π (ConvexPolygon.sum_interiorAngle_le), an ideal polygon has area (n - 2) π, and an ideal triangle has area π.

A polygon without ideal vertices is a compact convex polygon, whose area is CompactConvexPolygon.volume_carrier. A polygon with an ideal vertex has the area and angle sum of a convex polygon whose vertex 0 is ∞ (ConvexPolygon.exists_vertex_zero_eq_infty). For such a polygon the area of the part of the carrier to the left of the vertical through vertex k is the sum of the areas of the first k - 1 triangles of the fan from ∞ (ConvexPolygon.volume_carrier_inter_re_le_of_vertex_zero), and the angle sum is the sum of the finite angles of these triangles (ConvexPolygon.sum_interiorAngle_eq_of_vertex_zero). In these statements the vertices are indexed by natural numbers k, cast to Fin n under open Fin.NatCast.

Main results

• ConvexPolygon.volume_carrier: Gauss–Bonnet for convex polygons with ideal vertices.
• ConvexPolygon.volume_carrier_ne_top, ConvexPolygon.toReal_volume_carrier: the area is finite, equal to the angular defect.
• ConvexPolygon.sum_interiorAngle_le: the angular defect is nonnegative.
• ConvexPolygon.volume_carrier_of_forall_eq_inr: an ideal polygon has area (n - 2) π; ConvexPolygon.volume_carrier_three_of_forall_eq_inr: an ideal triangle has area π.
• ConvexPolygon.volume_carrier_three_of_vertex_one_of_vertex_two: a triangle with two ideal vertices has area π - α, for its angle α at the third vertex.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), Theorem 7.2.1 and Remark 2 after it (an ideal triangle has area π), Theorem 7.2.2 and its proof ("Cut up P into triangles. Apply Theorem 7.2.1 to each triangle and then sum the areas."), with ideal vertices as in §7.1; Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), Theorem 5.4.

A polygon with an ideal vertex at ∞

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sum_interiorAngle_eq_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) : ∑ i : Fin n, P.interiorAngle i = ∑ k ∈ Finset.Ico 1 (n - 1), (vertexAngle (P.vertex ↑k) (Sum.inr OnePoint.infty) (P.vertex (↑k + 1)) + vertexAngle (P.vertex (↑k + 1)) (P.vertex ↑k) (Sum.inr OnePoint.infty))

If vertex 0 is ∞, the angle sum is the sum of the finite angles of the triangles of the fan from ∞, indexed by the casts to Fin n of the natural numbers 1 ≤ k < n - 1.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_inter_re_le_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {k : ℕ} (hk : k ≠ 0) (hkn : k < n) : MeasureTheory.volume (P.carrier ∩ {z : UpperHalfPlane | z.re ≤ (toComplex (P.vertex ↑k)).re}) = ENNReal.ofReal (∑ j ∈ Finset.Ico 1 k, (Real.pi - vertexAngle (P.vertex ↑j) (Sum.inr OnePoint.infty) (P.vertex (↑j + 1)) - vertexAngle (P.vertex (↑j + 1)) (P.vertex ↑j) (Sum.inr OnePoint.infty)))

If vertex 0 is ∞, the area of the part of the carrier to the left of the vertical through vertex k, for 0 < k < n, is the sum of the areas π - αⱼ - βⱼ of the first k - 1 triangles of the fan from ∞, where αⱼ, βⱼ are the angles of the j-th triangle at vertex j and vertex (j + 1).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) : MeasureTheory.volume P.carrier = ENNReal.ofReal ((↑n - 2) * Real.pi - ∑ i : Fin n, P.interiorAngle i)

The Gauss–Bonnet formula for a convex polygon whose vertex 0 is ∞.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sum_interiorAngle_le_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) : ∑ i : Fin n, P.interiorAngle i ≤ (↑n - 2) * Real.pi

The angular defect of a convex polygon whose vertex 0 is ∞ is nonnegative.

Gauss–Bonnet

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) : MeasureTheory.volume P.carrier = ENNReal.ofReal ((↑n - 2) * Real.pi - ∑ i : Fin n, P.interiorAngle i)

The Gauss–Bonnet formula for convex hyperbolic polygons with ideal vertices: the area of a convex polygon with n vertices in ℍ ∪ ∂ℍ is (n - 2) π minus the sum of its interior angles, the angle at an ideal vertex being 0. Source: Walkden, Hyperbolic geometry (MATH32051), Theorem 7.2.2 and §7.1.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sum_interiorAngle_le {n : ℕ} [NeZero n] (P : ConvexPolygon n) : ∑ i : Fin n, P.interiorAngle i ≤ (↑n - 2) * Real.pi

The angular defect of a convex polygon is nonnegative: the sum of its interior angles is at most (n - 2) π.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_ne_top {n : ℕ} [NeZero n] (P : ConvexPolygon n) : MeasureTheory.volume P.carrier ≠ ⊤

A convex polygon has finite area.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.toReal_volume_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) : (MeasureTheory.volume P.carrier).toReal = (↑n - 2) * Real.pi - ∑ i : Fin n, P.interiorAngle i

The area of a convex polygon, as a real number, is its angular defect.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_of_forall_eq_inr {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : ∀ (i : Fin n), ∃ (ξ : OnePoint ℝ), P.vertex i = Sum.inr ξ) : MeasureTheory.volume P.carrier = ENNReal.ofReal ((↑n - 2) * Real.pi)

An ideal polygon, with all n vertices on ∂ℍ, has area (n - 2) π.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_three_of_forall_eq_inr (P : ConvexPolygon 3) (h : ∀ (i : Fin 3), ∃ (ξ : OnePoint ℝ), P.vertex i = Sum.inr ξ) : MeasureTheory.volume P.carrier = ENNReal.ofReal Real.pi

An ideal triangle has area π. Source: Walkden, Hyperbolic geometry (MATH32051), Remark 2 after Theorem 7.2.1.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_three_of_vertex_one_of_vertex_two (P : ConvexPolygon 3) {ξ η : OnePoint ℝ} (h₁ : P.vertex 1 = Sum.inr ξ) (h₂ : P.vertex 2 = Sum.inr η) : MeasureTheory.volume P.carrier = ENNReal.ofReal (Real.pi - P.interiorAngle 0)

A triangle with two ideal vertices has area π - α, for its angle α at the third vertex.