The Gauss–Bonnet formula for compact convex hyperbolic polygons

The invariant area of a compact convex hyperbolic polygon (all vertices in ℍ) with n vertices and interior angles α₀, …, αₙ₋₁ is (n - 2) π - (α₀ + ⋯ + αₙ₋₁) (CompactConvexPolygon.volume_carrier).

The file also provides the cut of a polygon along the diagonal from its penultimate vertex to vertex 0, used to argue by induction on the number of vertices (CompactConvexPolygon.induction): the first n - 1 vertices form a convex polygon (CompactConvexPolygon.eraseLast); seen from vertex 0 the vertices are in increasing angular order (CompactConvexPolygon.toReal_orientedAngle_lt); the diagonal has the last vertex strictly on its right and the vertices other than its two endpoints strictly on its left (CompactConvexPolygon.last_mem_rightHalfPlane_diagonal, CompactConvexPolygon.mem_leftHalfPlane_diagonal); the carrier is the union of the carrier of eraseLast and the triangle on the penultimate vertex, the last vertex and vertex 0 (CompactConvexPolygon.carrier_eq_union_triangle), which meet only on the line through the diagonal (CompactConvexPolygon.carrier_eraseLast_inter_triangle_subset); and the angle sum splits accordingly (CompactConvexPolygon.sum_interiorAngle_eq).

Main results

• CompactConvexPolygon.volume_carrier: Gauss–Bonnet for compact convex polygons (all vertices in ℍ), the area is (n - 2) π minus the sum of the interior angles.
• CompactConvexPolygon.sum_interiorAngle_le: the sum of the interior angles is at most (n - 2) π.
• CompactConvexPolygon.carrier_subset_closure_leftHalfPlane: the carrier lies in every closed half-plane containing the vertices.
• CompactConvexPolygon.isCompact_carrier: the carrier is compact.
• CompactConvexPolygon.induction: induction on the number of vertices, cutting off the last one.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), 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."). The bookkeeping of the cut is ours.

The angular order of the vertices seen from vertex 0

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_add_one_mem_leftHalfPlane {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {i k : Fin n} (hi : i ≠ k) (hi' : i ≠ k + 1) : P.vertex (k + 1) ∈ leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex k))

The convexity condition read cyclically: vertex (k + 1) lies to the left of the geodesic from vertex i to vertex k whenever i is neither k nor k + 1.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.toReal_orientedAngle_pos {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {j : Fin n} (hj₀ : j ≠ 0) (hj₁ : j ≠ 1) : 0 < ((P.vertex 0).orientedAngle (P.vertex 1) (P.vertex j)).toReal

Seen from vertex 0, every vertex other than vertex 0 and vertex 1 lies to the left of the first edge, so its oriented angle from the first edge is positive.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.toReal_orientedAngle_lt {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {j k : Fin n} (hj : j ≠ 0) (hjk : j < k) : ((P.vertex 0).orientedAngle (P.vertex 1) (P.vertex j)).toReal < ((P.vertex 0).orientedAngle (P.vertex 1) (P.vertex k)).toReal

Seen from vertex 0, the vertices are in increasing angular order.

Cutting off the last vertex

Throughout this section P : CompactConvexPolygon (n + 2) with 2 ≤ n, so P has at least four vertices: the penultimate one is P.vertex (Fin.castSucc (Fin.last n)) (index n) and the last one is P.vertex (Fin.last (n + 1)) (index n + 1). The diagonal from the penultimate vertex to vertex 0 cuts P into the polygon P.eraseLast hn : CompactConvexPolygon (n + 1) on the first n + 1 vertices, indexed through Fin.castSucc, and the triangle on the penultimate vertex, the last vertex and vertex 0.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.mem_leftHalfPlane_diagonal {n : ℕ} (P : CompactConvexPolygon (n + 2)) {j : Fin (n + 2)} (hj₀ : j ≠ 0) (hj : ↑j < n) : P.vertex j ∈ leftHalfPlane (geodesicBetween (P.vertex (Fin.last n).castSucc) (P.vertex 0))

Every vertex other than vertex 0 and the last two lies to the left of the diagonal from the penultimate vertex to vertex 0.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.last_mem_rightHalfPlane_diagonal {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : P.vertex (Fin.last (n + 1)) ∈ rightHalfPlane (geodesicBetween (P.vertex (Fin.last n).castSucc) (P.vertex 0))

The last vertex lies to the right of the diagonal from the penultimate vertex to vertex 0.

def TauCeti.UpperHalfPlane.CompactConvexPolygon.eraseLast {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : CompactConvexPolygon (n + 1)

The convex polygon on the first n + 1 vertices of a convex polygon with n + 2 ≥ 4 vertices.

Equations

• P.eraseLast hn = { vertex := P.vertex ∘ Fin.castSucc, three_le := ⋯, vertex_mem_leftHalfPlane := ⋯ }

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_eraseLast {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) (i : Fin (n + 1)) : (P.eraseLast hn).vertex i = P.vertex i.castSucc

The vertices of eraseLast.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.mem_carrier_eraseLast_iff {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) (z : UpperHalfPlane) : z ∈ (P.eraseLast hn).carrier ↔ (∀ (i : Fin (n + 2)), ↑i < n → z ∈ closure (leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))))) ∧ z ∈ closure (leftHalfPlane (geodesicBetween (P.vertex (Fin.last n).castSucc) (P.vertex 0)))

A point lies in the carrier of eraseLast if and only if it lies in the closed left half-planes of the first n edges and of the diagonal.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_eraseLast_inter_triangle_subset {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : (P.eraseLast hn).carrier ∩ (P.vertex (Fin.last n).castSucc).triangle (P.vertex (Fin.last (n + 1))) (P.vertex 0) ⊆ Set.range (geodesicLine (geodesicBetween (P.vertex (Fin.last n).castSucc) (P.vertex 0)))

The two pieces of the cut meet only on the geodesic line through the diagonal.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_zero_eq {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : P.interiorAngle 0 = (P.eraseLast hn).interiorAngle 0 + (P.vertex 0).interiorAngle (P.vertex (Fin.last n).castSucc) (P.vertex (Fin.last (n + 1)))

The interior angle at vertex 0 splits along the diagonal.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_penultimate_eq {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : P.interiorAngle (Fin.last n).castSucc = (P.eraseLast hn).interiorAngle (Fin.last n) + (P.vertex (Fin.last n).castSucc).interiorAngle (P.vertex 0) (P.vertex (Fin.last (n + 1)))

The interior angle at the penultimate vertex splits along the diagonal.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_last_eq {n : ℕ} (P : CompactConvexPolygon (n + 2)) : P.interiorAngle (Fin.last (n + 1)) = (P.vertex (Fin.last (n + 1))).interiorAngle (P.vertex (Fin.last n).castSucc) (P.vertex 0)

The interior angle at the last vertex is that of the triangle on the penultimate vertex, the last vertex and vertex 0.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_castSucc_eq {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) {i : Fin (n + 1)} (hi₀ : i ≠ 0) (hi : i ≠ Fin.last n) : P.interiorAngle i.castSucc = (P.eraseLast hn).interiorAngle i

The interior angles away from the diagonal are unchanged.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.sum_interiorAngle_eq {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : ∑ i : Fin (n + 2), P.interiorAngle i = ∑ i : Fin (n + 1), (P.eraseLast hn).interiorAngle i + ((P.vertex (Fin.last n).castSucc).interiorAngle (P.vertex (Fin.last (n + 1))) (P.vertex 0) + (P.vertex (Fin.last (n + 1))).interiorAngle (P.vertex 0) (P.vertex (Fin.last n).castSucc) + (P.vertex 0).interiorAngle (P.vertex (Fin.last n).castSucc) (P.vertex (Fin.last (n + 1))))

The sum of the interior angles splits along the diagonal.

Induction on the number of vertices

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.induction {n : ℕ} [NeZero n] {motive : {n : ℕ} → [inst : NeZero n] → CompactConvexPolygon n → Prop} (triangle : ∀ (Q : CompactConvexPolygon 3), motive Q) (eraseLast : ∀ {n : ℕ} (hn : 2 ≤ n) (Q : CompactConvexPolygon (n + 2)), motive (Q.eraseLast hn) → motive Q) (P : CompactConvexPolygon n) : motive P

To prove a property of every convex polygon, prove it for polygons with three vertices and show that it passes from Q.eraseLast hn to Q. In the inductive step `Q : CompactConvexPolygon (n

• 2)with2 ≤ nhas at least four vertices, andQ.eraseLast hn : CompactConvexPolygon (n + 1)is the polygon on its firstn + 1vertices: the vertex cut off isQ.vertex (Fin.last (n + 1)), and the last vertex of Q.eraseLast hnis the penultimate vertexQ.vertex (Fin.castSucc (Fin.last n))ofQ`.

The hull property and compactness

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_subset_closure_leftHalfPlane {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h : ∀ (i : Fin n), P.vertex i ∈ closure (leftHalfPlane g)) : P.carrier ⊆ closure (leftHalfPlane g)

The carrier lies in every closed half-plane containing the vertices.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_eq_union_triangle {n : ℕ} (P : CompactConvexPolygon (n + 2)) (hn : 2 ≤ n) : P.carrier = (P.eraseLast hn).carrier ∪ (P.vertex (Fin.last n).castSucc).triangle (P.vertex (Fin.last (n + 1))) (P.vertex 0)

The carrier of a convex polygon is the union of the carrier of eraseLast and the triangle on the penultimate vertex, the last vertex and vertex 0.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.isCompact_carrier {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : IsCompact P.carrier

The carrier is compact.

Gauss–Bonnet

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

The Gauss–Bonnet formula for compact convex polygons (all vertices in ℍ) together with the nonnegativity of the angular defect, the form in which the induction runs.

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

The Gauss–Bonnet formula for compact convex hyperbolic polygons: the area of a convex polygon with n vertices, all in ℍ (no ideal vertices), is (n - 2) π minus the sum of its interior angles. Source: Walkden, Hyperbolic geometry (MATH32051), Theorem 7.2.2.

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

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