A convex polygon with an ideal vertex at ∞

Let P be a convex polygon whose vertex 0 is the ideal point ∞. Its sides from ∞ to vertex 1 and from vertex (-1) back to ∞ are vertical lines, and every other side runs along a semicircle with ∞ on its left, from left to right. Writing xᵢ for the real part of toComplex (vertex i), which is the real coordinate of vertex i for i ≠ 0 (for i = 0 it is the junk value 0), the real parts x₁ < ⋯ < xₙ₋₁ increase strictly and the carrier lies between the verticals through vertex 1 and vertex (-1). Between the verticals through vertex i and vertex (i + 1), for i ≠ 0, -1, the carrier is the hyperbolic triangle with vertices ∞, vertex i and vertex (i + 1): the region above the semicircle of the side i. These triangles form the fan of diagonals from the ideal vertex ∞, and the interior angle of P at each vertex other than ∞, vertex 1 and vertex (-1) is the sum of the angles of the two triangles of the fan meeting there.

Main results

• ConvexPolygon.sideForm_sideGeodesic_zero_of_vertex_zero, ConvexPolygon.sideForm_sideGeodesic_neg_one_of_vertex_zero: the two sides at ∞ lie on vertical lines.
• ConvexPolygon.exists_sideForm_sideGeodesic_eq_of_vertex_zero, ConvexPolygon.re_toComplex_vertex_lt_of_vertex_zero: every other side is a semicircle with ∞ on its left, running from left to right.
• ConvexPolygon.re_toComplex_vertex_lt_of_lt: the real parts of vertex 1, …, vertex (n - 1) increase strictly.
• ConvexPolygon.re_toComplex_vertex_one_le_of_mem_carrier, ConvexPolygon.re_le_re_toComplex_vertex_neg_one_of_mem_carrier: the carrier lies between the verticals through vertex 1 and vertex (-1).
• ConvexPolygon.exists_carrier_inter_strip_eq: between the verticals through vertex i and vertex (i + 1), the carrier is the region above the semicircle of the side i (idealRegionAbove).
• ConvexPolygon.volume_carrier_inter_strip: the area of this triangle is π minus its angles at vertex i and vertex (i + 1), which sum to at most π (ConvexPolygon.vertexAngle_add_vertexAngle_le_pi_of_vertex_zero).
• ConvexPolygon.interiorAngle_eq_add_of_vertex_zero: the upward vertical splits the interior angle at a vertex other than ∞, vertex 1 and vertex (-1) into the angles of the two adjacent triangles.
• ConvexPolygon.exists_vertex_zero_eq_infty, ConvexPolygon.exists_vertex_zero_eq_infty_of_not_forall_eq_inl: a convex polygon with an ideal vertex has the area and angle sum of a convex polygon whose vertex 0 is ∞.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), the proof of Theorem 7.2.1 in the case of a vertex on ∂ℍ (map it to ∞; the other two vertices lie on a semicircle; the area is ∫ₐᵇ dx / √(1 - x²) = π - (α + β)), and Theorem 7.2.2 ("Cut up P into triangles. Apply Theorem 7.2.1 to each triangle and then sum the areas."); Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), §5, proof of Theorem 5.4.

The sides

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_ne_inr_infty_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) : P.vertex i ≠ Sum.inr OnePoint.infty

If vertex 0 is ∞, no other vertex is.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideForm_sideGeodesic_zero_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) (z : ℂ) : sideForm (P.sideGeodesic 0) z = (toComplex (P.vertex 1)).re - z.re

If vertex 0 is ∞, the side from ∞ down to vertex 1 is the vertical line through vertex 1, with side form x₁ - Re z.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideForm_sideGeodesic_neg_one_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) (z : ℂ) : sideForm (P.sideGeodesic (-1)) z = z.re - (toComplex (P.vertex (-1))).re

If vertex 0 is ∞, the side from vertex (-1) up to ∞ is the vertical line through vertex (-1), with side form Re z - xₙ₋₁.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.infty_mem_boundaryLeftHalfPlane_sideGeodesic_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : OnePoint.infty ∈ boundaryLeftHalfPlane (P.sideGeodesic i)

If vertex 0 is ∞, it lies strictly to the left of every side not ending at it.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.re_toComplex_vertex_lt_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : (toComplex (P.vertex i)).re < (toComplex (P.vertex (i + 1))).re

If vertex 0 is ∞, every side not ending at ∞ runs from left to right.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_sideForm_sideGeodesic_eq_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : ∃ (m : ℝ) (ρ : ℝ) (κ : ℝ), 0 < ρ ∧ 0 < κ ∧ ∀ (z : ℂ), sideForm (P.sideGeodesic i) z = κ * (ρ ^ 2 - Complex.normSq (z - ↑m))

If vertex 0 is ∞, every side not ending at ∞ is a semicircle with ∞ on its left: its side form is a positive multiple of ρ² - |z - m|² for its centre m and radius ρ > 0.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.re_toComplex_vertex_lt_of_lt {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i j : Fin n} (hi : i ≠ 0) (hij : i < j) : (toComplex (P.vertex i)).re < (toComplex (P.vertex j)).re

If vertex 0 is ∞, the real parts of vertex 1, …, vertex (n - 1) increase strictly.

The carrier

theorem TauCeti.UpperHalfPlane.ConvexPolygon.re_toComplex_vertex_one_le_of_mem_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {z : UpperHalfPlane} (hz : z ∈ P.carrier) : (toComplex (P.vertex 1)).re ≤ z.re

If vertex 0 is ∞, the carrier lies to the right of the vertical through vertex 1.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.re_le_re_toComplex_vertex_neg_one_of_mem_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {z : UpperHalfPlane} (hz : z ∈ P.carrier) : z.re ≤ (toComplex (P.vertex (-1))).re

If vertex 0 is ∞, the carrier lies to the left of the vertical through vertex (-1).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_carrier_inter_strip_eq {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : ∃ (m : ℝ) (ρ : ℝ), 0 < ρ ∧ Complex.normSq (toComplex (P.vertex i) - ↑m) = ρ ^ 2 ∧ Complex.normSq (toComplex (P.vertex (i + 1)) - ↑m) = ρ ^ 2 ∧ P.carrier ∩ {z : UpperHalfPlane | (toComplex (P.vertex i)).re ≤ z.re ∧ z.re ≤ (toComplex (P.vertex (i + 1))).re} = idealRegionAbove m ρ (toComplex (P.vertex i)).re (toComplex (P.vertex (i + 1))).re

The triangles of the fan from ∞. If vertex 0 is ∞, then between the verticals through vertex i and vertex (i + 1), for an side i not ending at ∞, the carrier is the region above the semicircle of that side, of centre m and radius ρ, through both vertices.

The centre and radius are shared by the four conclusions, which are therefore stated together.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_inter_strip {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : MeasureTheory.volume (P.carrier ∩ {z : UpperHalfPlane | (toComplex (P.vertex i)).re ≤ z.re ∧ z.re ≤ (toComplex (P.vertex (i + 1))).re}) = ENNReal.ofReal (Real.pi - vertexAngle (P.vertex i) (Sum.inr OnePoint.infty) (P.vertex (i + 1)) - vertexAngle (P.vertex (i + 1)) (P.vertex i) (Sum.inr OnePoint.infty))

Gauss–Bonnet for the triangles of the fan from ∞. If vertex 0 is ∞, the part of the carrier between the verticals through vertex i and vertex (i + 1), for an side i not ending at ∞, has area π minus the angles at vertex i and vertex (i + 1) of the triangle with vertices ∞, vertex i, vertex (i + 1). That part of the carrier is this triangle by exists_carrier_inter_strip_eq.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexAngle_add_vertexAngle_le_pi_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) : vertexAngle (P.vertex i) (Sum.inr OnePoint.infty) (P.vertex (i + 1)) + vertexAngle (P.vertex (i + 1)) (P.vertex i) (Sum.inr OnePoint.infty) ≤ Real.pi

The two finite angles of a triangle of the fan from ∞ sum to at most π.

The interior angles

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_eq_add_of_vertex_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty) {i : Fin n} (hi : i ≠ 0) (hi₁ : i - 1 ≠ 0) (hi' : i + 1 ≠ 0) : P.interiorAngle i = vertexAngle (P.vertex i) (P.vertex (i - 1)) (Sum.inr OnePoint.infty) + vertexAngle (P.vertex i) (Sum.inr OnePoint.infty) (P.vertex (i + 1))

If vertex 0 is ∞, the interior angle at a vertex other than ∞, vertex 1 and vertex (-1) is split by the upward vertical into the angles of the two triangles of the fan from ∞ meeting there.

Moving an ideal vertex to ∞

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_vertex_zero_eq_infty {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} {ξ : OnePoint ℝ} (hi : P.vertex i = Sum.inr ξ) : ∃ (Q : ConvexPolygon n), Q.vertex 0 = Sum.inr OnePoint.infty ∧ MeasureTheory.volume Q.carrier = MeasureTheory.volume P.carrier ∧ ∑ j : Fin n, Q.interiorAngle j = ∑ j : Fin n, P.interiorAngle j

A convex polygon whose vertex i is an ideal point ξ has the area and angle sum of some convex polygon with vertex 0 = ∞.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_vertex_zero_eq_infty_of_not_forall_eq_inl {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : ¬∀ (i : Fin n), ∃ (z : UpperHalfPlane), P.vertex i = Sum.inl z) : ∃ (Q : ConvexPolygon n), Q.vertex 0 = Sum.inr OnePoint.infty ∧ MeasureTheory.volume Q.carrier = MeasureTheory.volume P.carrier ∧ ∑ j : Fin n, Q.interiorAngle j = ∑ j : Fin n, P.interiorAngle j

A convex polygon some vertex of which does not lie in ℍ has the area and angle sum of some convex polygon with vertex 0 = ∞.