The area of a hyperbolic triangle with a vertex at infinity

idealRegion a b is the region of ℍ above the unit semicircle and between the vertical lines re = a and re = b. For -1 ≤ a ≤ b ≤ 1 it is a hyperbolic triangle with vertices a + i √(1 - a²), b + i √(1 - b²) and the point at infinity, and its invariant area is arccos a - arccos b (volume_idealRegion); this is the base case of the Gauss–Bonnet formula, in which the two finite angles are arccos (-a) and arccos b. For a = -1 (respectively b = 1) the left (respectively right) vertex is the ideal point -1 (respectively 1), with angle 0; in particular the ideal triangle with vertices -1, 1 and ∞ has area π (volume_idealRegion_neg_one_one). Vertical lines are null (volume_setOf_re_eq).

idealRegionAbove c r a b is the same region for the semicircle of centre c and radius r > 0, obtained from idealRegion by the affine map z ↦ r z + c (idealRegionAbove_eq_smul); its area is the same formula in the rescaled endpoints when c - r ≤ a ≤ b ≤ c + r (volume_idealRegionAbove). The two one-variable integrals of the computation are TauCeti.lintegral_Ioi_inv_sq and TauCeti.integral_one_div_sqrt_one_sub_sq.

Source: Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), §5: the area μ(A) = ∫_A dx dy / y² (5.1) and its invariance (Theorem 5.3), p. 18; the computation μ(Δ) = ∫_a^b dx / √(1 - x²) = π - α - β for a triangle with a vertex at ∞, p. 19–20.

def TauCeti.UpperHalfPlane.idealRegion (a b : ℝ) : Set UpperHalfPlane

The region above the unit semicircle between the verticals re = a and re = b.

Equations

• TauCeti.UpperHalfPlane.idealRegion a b = {z : UpperHalfPlane | a ≤ z.re ∧ z.re ≤ b ∧ 1 ≤ Complex.normSq ↑z}

@[simp]

theorem TauCeti.UpperHalfPlane.mem_idealRegion_iff (a b : ℝ) (z : UpperHalfPlane) : z ∈ idealRegion a b ↔ a ≤ z.re ∧ z.re ≤ b ∧ 1 ≤ Complex.normSq ↑z

Membership in idealRegion a b.

theorem TauCeti.UpperHalfPlane.measurableSet_idealRegion (a b : ℝ) : MeasurableSet (idealRegion a b)

idealRegion a b is measurable.

theorem TauCeti.UpperHalfPlane.volume_setOf_re_eq (x : ℝ) : MeasureTheory.volume {z : UpperHalfPlane | z.re = x} = 0

A vertical line is a null set.

theorem TauCeti.UpperHalfPlane.volume_idealRegion {a b : ℝ} (ha : -1 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) : MeasureTheory.volume (idealRegion a b) = ENNReal.ofReal (Real.arccos a - Real.arccos b)

The area of a hyperbolic triangle with a vertex at infinity, in normal form: the region above the unit semicircle between the verticals re = a and re = b has invariant area arccos a - arccos b, for -1 ≤ a ≤ b ≤ 1. For a = -1 (respectively b = 1) the left (respectively right) vertex is the ideal point -1 (respectively 1), with angle 0.

theorem TauCeti.UpperHalfPlane.volume_idealRegion_neg_one_one : MeasureTheory.volume (idealRegion (-1) 1) = ENNReal.ofReal Real.pi

The area of the ideal triangle with vertices -1, 1 and ∞ is π.

def TauCeti.UpperHalfPlane.idealRegionAbove (c r a b : ℝ) : Set UpperHalfPlane

The region above the semicircle of centre c and radius r between the verticals re = a and re = b.

Equations

• TauCeti.UpperHalfPlane.idealRegionAbove c r a b = {z : UpperHalfPlane | a ≤ z.re ∧ z.re ≤ b ∧ r ^ 2 ≤ Complex.normSq (↑z - ↑c)}

@[simp]

theorem TauCeti.UpperHalfPlane.mem_idealRegionAbove_iff (c r a b : ℝ) (z : UpperHalfPlane) : z ∈ idealRegionAbove c r a b ↔ a ≤ z.re ∧ z.re ≤ b ∧ r ^ 2 ≤ Complex.normSq (↑z - ↑c)

Membership in idealRegionAbove c r a b.

theorem TauCeti.UpperHalfPlane.measurableSet_idealRegionAbove (c r a b : ℝ) : MeasurableSet (idealRegionAbove c r a b)

idealRegionAbove c r a b is measurable.

theorem TauCeti.UpperHalfPlane.idealRegionAbove_eq_smul {c r : ℝ} (hr : 0 < r) (a b : ℝ) : idealRegionAbove c r a b = (Matrix.ProjectiveSpecialLinearGroup.upperRightHom c * ↑(Matrix.SpecialLinearGroup.dilation (Real.log r))) • idealRegion ((a - c) / r) ((b - c) / r)

idealRegionAbove c r a b is the image of idealRegion under the affine map z ↦ r z + c.

theorem TauCeti.UpperHalfPlane.volume_idealRegionAbove {c r a b : ℝ} (hr : 0 < r) (ha : c - r ≤ a) (hab : a ≤ b) (hb : b ≤ c + r) : MeasureTheory.volume (idealRegionAbove c r a b) = ENNReal.ofReal (Real.arccos ((a - c) / r) - Real.arccos ((b - c) / r))

The area of a hyperbolic triangle with a vertex at infinity, for a general semicircle, for c - r ≤ a ≤ b ≤ c + r.

theorem TauCeti.UpperHalfPlane.volume_range_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : MeasureTheory.volume (Set.range (geodesicLine g)) = 0

A geodesic line is a null set.