Hyperbolic triangles and the Gauss–Bonnet formula #
A hyperbolic triangle with vertices A, B, C in ℍ is the intersection of the three closed
half-planes bounded by the geodesic through two of the vertices and containing the third
(triangle). Its interior angle at A is interiorAngle A B C, the angle between the
geodesics from A to B and from A to C (defined in Geodesic/InteriorAngle.lean). The
Gauss–Bonnet formula (volume_triangle) computes its invariant area as the angular defect
π - α - β - γ.
The point-keyed API lives in the UpperHalfPlane namespace: UpperHalfPlane.closedSide,
UpperHalfPlane.triangle. Membership is read off with
UpperHalfPlane.mem_closedSide_iff and UpperHalfPlane.mem_triangle_iff. A triangle contains its
vertices (UpperHalfPlane.left_mem_triangle), is invariant under cyclic permutation of them
(UpperHalfPlane.triangle_rotate) and, when nondegenerate, under every transposition
(UpperHalfPlane.triangle_swap_left, UpperHalfPlane.triangle_swap_right,
UpperHalfPlane.triangle_reverse). An interior angle is the Euclidean angle between any positive
multiples of the two velocities (interiorAngle_eq_angle_of_velocity_eq).
Following Katok, the formula is first proved for triangles with a vertex at infinity
(volume_idealRegion), and a general triangle is the difference of two such, cut along the
geodesic through one vertex and the point at infinity of the opposite side. We normalise so that
this point at infinity is ∞ itself: the side AB lies on the imaginary axis, and C lies to
its right (exists_smul_eq_normal_form). In this normal form the triangle is described by
three explicit inequalities (mem_triangle_normal_form_iff), it differs from Δ₁ \ Δ₂ by a null
arc (triangle_subset_diff_union_of_normal_form), and its three interior angles are read off the
radius vectors of the two semicircles (interiorAngle_I_geodesicLine_one,
interiorAngle_geodesicLine_one_I, interiorAngle_of_normal_form). The comparison of the two
discs uses the radical-line identity Complex.normSq_sub_ofReal_sub_normSq_sub_ofReal.
Source: Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), §5 p. 19–20: the definition of a hyperbolic triangle and Theorem 5.4 (Gauss–Bonnet) with its proof.
The closed half-plane bounded by the geodesic through two points #
The closed half-plane bounded by the geodesic from z to w that contains u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restatement of the body of closedSide, unfolded from the def.
Membership in a closed side: it is the closed right half-plane of the geodesic from z to
w when u lies in the open right half-plane, and the closed left half-plane otherwise.
The reference point lies in its closed side.
The bounding line lies in the closed side.
Closed sides are closed.
Closed sides are measurable.
The closed side does not depend on the direction of the bounding geodesic, as long as the reference point is off the line.
Triangles #
The hyperbolic triangle with vertices A, B, C: the intersection of the three closed
half-planes bounded by the geodesic through two vertices and containing the third.
Equations
- A.triangle B C = A.closedSide B C ∩ B.closedSide C A ∩ C.closedSide A B
Instances For
Restatement of the body of triangle, unfolded from the def.
A point lies in the triangle A B C when it lies in each of its three closed sides.
Triangles are closed.
Triangles are measurable.
The triangle is invariant under cyclic permutation of its vertices.
A triangle contains its first vertex; by triangle_rotate, it contains all three.
The triangle does not depend on the order of its first two vertices, as long as the third is off the line through them.
The nondegenerate triangle does not depend on the order of its last two vertices.
The nondegenerate triangle does not depend on the order of its first and last vertices: it is unchanged by reversing the order of the vertices.
Invariance under the action #
Closed sides transform naturally under the action.
The Gauss–Bonnet formula #
The triangle in normal form, with A = I, B = i exp d above it and C to the right, as
a system of inequalities: to the right of the imaginary axis, inside the disc bounded by the
semicircle through B and C, and outside the disc bounded by the semicircle through I and
C.
In normal form, the centre of the semicircle through i exp d and C lies to the left of
the centre of the semicircle through I and C.
If the velocities at P of the geodesics to Q₁ and Q₂ are positive multiples of v₁ and
v₂, the interior angle at P is the Euclidean angle between v₁ and v₂.
The interior angle at I of the triangle in normal form.
The interior angle at i exp d of the triangle in normal form.
The interior angle at C of the triangle in normal form: the difference of the angles
between the vertical through C and the two semicircles.
The angle sum of the triangle in normal form, with vertices I, geodesicLine 1 d and C,
is at most π, for 0 < d and 0 < C.re.
The Gauss–Bonnet formula for the triangle in normal form.
Every nondegenerate triangle can be moved to normal form, possibly after swapping A and
B.
The Gauss–Bonnet formula: the invariant area of a hyperbolic triangle is its angular
defect π - α - β - γ.
The angular defect of a nondegenerate triangle is nonnegative: the sum of its angles is at
most π.
Source: Katok, Fuchsian groups, geodesic flows… (Clay Math. Proc. 10), p. 20.