Geodesic segments and the convexity of half-planes

UpperHalfPlane.geodesicSegment z w is the geodesic segment from z to w: the image of [0, dist z w] under the geodesic line geodesicBetween z w. The point-keyed API lives in the UpperHalfPlane namespace (UpperHalfPlane.mem_geodesicSegment_iff, UpperHalfPlane.geodesicSegment_comm, UpperHalfPlane.isCompact_geodesicSegment, …), and segments transform naturally under PSL(2, ℝ) (smul_geodesicSegment).

Along any geodesic line the real part is monotone or antitone (monotone_re_geodesicLine_or_antitone); the set of parameters at which a geodesic line lies in a given half-plane or its closure is an interval (ordConnected_preimage_geodesicLine_rightHalfPlane and companions); and half-planes and their closures are convex: they contain the segment between any two of their points (geodesicSegment_subset_rightHalfPlane, …, geodesicSegment_subset_closure_leftHalfPlane). Convexity is what makes the triangles and polygons bounded by such half-planes convex. An interior point of an interval in a closed half-plane lies in the open half-plane unless the supporting lines coincide (geodesicLine_mem_leftHalfPlane_of_mem_closure).

Source: Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (the segment [z, w]) and Solution 14.1 (half-planes are convex); Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), Theorem 3.1 p. 10 (geodesics are semicircles and vertical rays).

Segments

def UpperHalfPlane.geodesicSegment (z w : UpperHalfPlane) : Set UpperHalfPlane

The geodesic segment from z to w.

Equations

• z.geodesicSegment w = TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween z w) '' Set.Icc 0 (dist z w)

theorem UpperHalfPlane.geodesicSegment_def (z w : UpperHalfPlane) : z.geodesicSegment w = TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween z w) '' Set.Icc 0 (dist z w)

The geodesic segment from z to w, unfolded: the image of [0, dist z w] under the geodesic line from z to w.

theorem UpperHalfPlane.mem_geodesicSegment_iff (z w u : UpperHalfPlane) : u ∈ z.geodesicSegment w ↔ ∃ t ∈ Set.Icc 0 (dist z w), TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween z w) t = u

Membership in geodesicSegment z w.

@[simp]

theorem UpperHalfPlane.left_mem_geodesicSegment (z w : UpperHalfPlane) : z ∈ z.geodesicSegment w

z lies on the segment from z to w.

@[simp]

theorem UpperHalfPlane.right_mem_geodesicSegment (z w : UpperHalfPlane) : w ∈ z.geodesicSegment w

w lies on the segment from z to w.

@[simp]

theorem UpperHalfPlane.geodesicSegment_self (z : UpperHalfPlane) : z.geodesicSegment z = {z}

The segment from a point to itself is that point.

theorem UpperHalfPlane.geodesicSegment_subset_range_geodesicLine (z w : UpperHalfPlane) : z.geodesicSegment w ⊆ Set.range (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween z w))

A segment lies on the geodesic line through its endpoints.

theorem UpperHalfPlane.geodesicSegment_comm (z w : UpperHalfPlane) : w.geodesicSegment z = z.geodesicSegment w

The segment does not depend on the order of its endpoints.

theorem UpperHalfPlane.isCompact_geodesicSegment (z w : UpperHalfPlane) : IsCompact (z.geodesicSegment w)

Segments are compact.

theorem UpperHalfPlane.isClosed_geodesicSegment (z w : UpperHalfPlane) : IsClosed (z.geodesicSegment w)

Segments are closed.

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicSegment_geodesicLine {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {s t : ℝ} : (geodesicLine g s).geodesicSegment (geodesicLine g t) = geodesicLine g '' Set.uIcc s t

The segment between two points of a unit-speed geodesic is the image of the interval between their parameters. The parameters may be given in either order.

@[simp]

theorem TauCeti.UpperHalfPlane.smul_geodesicSegment (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z w : UpperHalfPlane) : h • z.geodesicSegment w = (h • z).geodesicSegment (h • w)

Segments transform naturally under the action.

The real part is monotone along a geodesic line

theorem TauCeti.UpperHalfPlane.monotone_re_geodesicLine_or_antitone (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (Monotone fun (t : ℝ) => (geodesicLine g t).re) ∨ Antitone fun (t : ℝ) => (geodesicLine g t).re

Along a geodesic line the real part is monotone or antitone: the line is a vertical ray or a semicircle centred on the real axis, traversed once. Source: Katok, Fuchsian groups, geodesic flows… (Clay Math. Proc. 10), Theorem 3.1 p. 10.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_rightHalfPlane (g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (geodesicLine g ⁻¹' rightHalfPlane k).OrdConnected

The parameters at which a geodesic line lies in an open right half-plane form an interval.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_closure_rightHalfPlane (g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (geodesicLine g ⁻¹' closure (rightHalfPlane k)).OrdConnected

The parameters at which a geodesic line lies in the closure of a right half-plane form an interval.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_leftHalfPlane (g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (geodesicLine g ⁻¹' leftHalfPlane k).OrdConnected

The parameters at which a geodesic line lies in an open left half-plane form an interval.

theorem TauCeti.UpperHalfPlane.ordConnected_preimage_geodesicLine_closure_leftHalfPlane (g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (geodesicLine g ⁻¹' closure (leftHalfPlane k)).OrdConnected

The parameters at which a geodesic line lies in the closure of a left half-plane form an interval.

theorem TauCeti.UpperHalfPlane.geodesicLine_mem_leftHalfPlane_of_mem_closure {g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {s u t : ℝ} (hsu : s < u) (hut : u < t) (hs : geodesicLine g s ∈ closure (leftHalfPlane k)) (ht : geodesicLine g t ∈ closure (leftHalfPlane k)) (hne : Set.range (geodesicLine g) ≠ Set.range (geodesicLine k)) : geodesicLine g u ∈ leftHalfPlane k

An interior point of a geodesic interval in a closed half-plane is strictly in that half-plane unless the two supporting geodesic lines coincide.

Half-planes are convex

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_rightHalfPlane {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hz : z ∈ rightHalfPlane k) (hw : w ∈ rightHalfPlane k) : z.geodesicSegment w ⊆ rightHalfPlane k

Open right half-planes are convex. Source: Walkden, Hyperbolic geometry (MATH32051), Solution 14.1.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_closure_rightHalfPlane {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hz : z ∈ closure (rightHalfPlane k)) (hw : w ∈ closure (rightHalfPlane k)) : z.geodesicSegment w ⊆ closure (rightHalfPlane k)

Closed right half-planes are convex.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_leftHalfPlane {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hz : z ∈ leftHalfPlane k) (hw : w ∈ leftHalfPlane k) : z.geodesicSegment w ⊆ leftHalfPlane k

Open left half-planes are convex.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_closure_leftHalfPlane {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hz : z ∈ closure (leftHalfPlane k)) (hw : w ∈ closure (leftHalfPlane k)) : z.geodesicSegment w ⊆ closure (leftHalfPlane k)

Closed left half-planes are convex.