Compact convex hyperbolic polygons

A compact convex hyperbolic polygon with n ≥ 3 vertices is given by its vertices v₀, …, vₙ₋₁ ∈ ℍ, listed counterclockwise: every vertex other than the endpoints of an edge lies strictly to the left of the geodesic through that edge (CompactConvexPolygon). Its carrier is the intersection of the closed left half-planes of its edges (CompactConvexPolygon.carrier), its sides are the geodesic segments between consecutive vertices (CompactConvexPolygon.side, via UpperHalfPlane.geodesicSegment), and its interior angle at a vertex is the angle between the two sides at that vertex (CompactConvexPolygon.interiorAngle).

All vertices lie in ℍ, so every interior angle is positive (and the carrier is compact, CompactConvexPolygon.isCompact_carrier in Polygon/GaussBonnet.lean). Hyperbolic polygons in general may also have ideal vertices on ∂ℍ, with interior angle 0 (Walkden §7.1); those are not covered here.

Main results

• CompactConvexPolygon.vertex_injective: the vertices are distinct.
• CompactConvexPolygon.isClosed_carrier, CompactConvexPolygon.vertex_mem_carrier, CompactConvexPolygon.side_subset_carrier, CompactConvexPolygon.geodesicSegment_subset_carrier: the carrier is closed and convex and contains the vertices and the sides.
• CompactConvexPolygon.interiorAngle_pos, CompactConvexPolygon.interiorAngle_lt_pi: the interior angles lie strictly between 0 and π.
• The MulAction of PSL(2, ℝ) on compact convex polygons, with CompactConvexPolygon.vertex_smul, CompactConvexPolygon.carrier_smul, CompactConvexPolygon.side_smul, CompactConvexPolygon.interiorAngle_smul: everything transforms naturally under PSL(2, ℝ).
• CompactConvexPolygon.carrier_three, CompactConvexPolygon.sum_interiorAngle_three: a polygon with three vertices is the triangle on them, with the same angles.

The counterclockwise orientation is a convention of this file: a clockwise list of vertices is not a CompactConvexPolygon.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (polygons with given vertices) and §14.2 (a convex hyperbolic polygon is an intersection of finitely many half-planes).

structure TauCeti.UpperHalfPlane.CompactConvexPolygon (n : ℕ) [NeZero n] : Type

A compact convex hyperbolic polygon: a convex hyperbolic polygon with n vertices vertex 0, …, vertex (n - 1), all in ℍ (no ideal vertices), listed counterclockwise: every vertex other than vertex i and vertex (i + 1) lies strictly to the left of the geodesic from vertex i to vertex (i + 1).

• vertex : Fin n → UpperHalfPlane

  The vertices, in counterclockwise order; indices are taken cyclically.

• three_le : 3 ≤ n

  A polygon has at least three vertices.

• vertex_mem_leftHalfPlane (i j : Fin n) : j ≠ i → j ≠ i + 1 → self.vertex j ∈ leftHalfPlane (geodesicBetween (self.vertex i) (self.vertex (i + 1)))

  Every vertex off an edge lies strictly to the left of it.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.ext_iff {n : ℕ} {inst✝ : NeZero n} {x y : CompactConvexPolygon n} : x = y ↔ x.vertex = y.vertex

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.ext {n : ℕ} {inst✝ : NeZero n} {x y : CompactConvexPolygon n} (vertex : x.vertex = y.vertex) : x = y

def TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : Set UpperHalfPlane

The carrier of a convex polygon: the intersection of the closed left half-planes of its edges.

Equations

• P.carrier = ⋂ (i : Fin n), closure (TauCeti.UpperHalfPlane.leftHalfPlane (TauCeti.UpperHalfPlane.geodesicBetween (P.vertex i) (P.vertex (i + 1))))

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_def {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : P.carrier = ⋂ (i : Fin n), closure (leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))))

The carrier, unfolded: the intersection of the closed left half-planes of the edges.

def TauCeti.UpperHalfPlane.CompactConvexPolygon.side {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : Set UpperHalfPlane

The side of a convex polygon from vertex i to vertex (i + 1).

Equations

• P.side i = (P.vertex i).geodesicSegment (P.vertex (i + 1))

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.side_def {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.side i = (P.vertex i).geodesicSegment (P.vertex (i + 1))

The side of a convex polygon, unfolded: the geodesic segment from vertex i to vertex (i + 1).

noncomputable def TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : ℝ

The interior angle of a convex polygon at vertex i: the angle between the sides to vertex (i - 1) and to vertex (i + 1).

Equations

• P.interiorAngle i = (P.vertex i).interiorAngle (P.vertex (i - 1)) (P.vertex (i + 1))

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_def {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.interiorAngle i = (P.vertex i).interiorAngle (P.vertex (i - 1)) (P.vertex (i + 1))

The interior angle of a convex polygon, unfolded.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.mem_carrier_iff {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (z : UpperHalfPlane) : z ∈ P.carrier ↔ ∀ (i : Fin n), z ∈ closure (leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))))

Membership in the carrier.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_notMem_range_geodesicLine {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {i j : Fin n} (hi : j ≠ i) (hi' : j ≠ i + 1) : P.vertex j ∉ Set.range (geodesicLine (geodesicBetween (P.vertex i) (P.vertex (i + 1))))

A vertex off an edge is not on the geodesic through that edge.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_injective {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : Function.Injective P.vertex

The vertices of a convex polygon are distinct.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_ne_vertex_add_one {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.vertex i ≠ P.vertex (i + 1)

A vertex differs from the next one.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_ne_vertex_sub_one {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.vertex i ≠ P.vertex (i - 1)

A vertex differs from the previous one.

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

The carrier is closed.

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

The carrier is measurable.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_mem_carrier {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.vertex i ∈ P.carrier

The vertices lie in the carrier.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_mem_closure_leftHalfPlane {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i j : Fin n) : P.vertex j ∈ closure (leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))))

Every vertex lies in the closed left half-plane of every edge.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.geodesicSegment_subset_carrier {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) {z w : UpperHalfPlane} (hz : z ∈ P.carrier) (hw : w ∈ P.carrier) : z.geodesicSegment w ⊆ P.carrier

The carrier is convex.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.side_subset_carrier {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.side i ⊆ P.carrier

The sides lie in the carrier.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_pos {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : 0 < P.interiorAngle i

The interior angles are positive.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_lt_pi {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.interiorAngle i < Real.pi

The interior angles are less than π.

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfPlane.CompactConvexPolygon.instMulActionProjectiveSpecialLinearGroupFinOfNatNatReal {n : ℕ} [NeZero n] : MulAction (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (CompactConvexPolygon n)

PSL(2, ℝ) acts on compact convex polygons by moving their vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_smul {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).vertex i = h • P.vertex i

The vertices of the translate.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_smul {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (h • P).carrier = h • P.carrier

The carrier of the translate is the translate of the carrier.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.side_smul {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).side i = h • P.side i

The sides of the translate are the translates of the sides.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_smul {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).interiorAngle i = P.interiorAngle i

The interior angles are invariant under PSL(2, ℝ).

Polygons with three vertices

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_three (P : CompactConvexPolygon 3) : P.carrier = (P.vertex 0).triangle (P.vertex 1) (P.vertex 2)

The carrier of a polygon with three vertices is the triangle on them.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_three (P : CompactConvexPolygon 3) (i : Fin 3) : P.interiorAngle i = (P.vertex i).interiorAngle (P.vertex (i + 1)) (P.vertex (i + 2))

The interior angles of a polygon with three vertices are the angles of the triangle on them, read counterclockwise from each vertex.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.sum_interiorAngle_three (P : CompactConvexPolygon 3) : ∑ i : Fin 3, P.interiorAngle i = (P.vertex 0).interiorAngle (P.vertex 1) (P.vertex 2) + (P.vertex 1).interiorAngle (P.vertex 2) (P.vertex 0) + (P.vertex 2).interiorAngle (P.vertex 0) (P.vertex 1)

The sum of the interior angles of a polygon with three vertices is the angle sum of the triangle on them.