Half-planes bounded by a geodesic line #
The imaginary axis splits ℍ into two open half-planes, {z | 0 < z.re} and
{z | z.re < 0}, and the axis itself, {z | z.re = 0}. This file transports that picture by
g : PSL(2, ℝ), the same idiom Geodesic.lean uses for the line itself: rightHalfPlane g
and leftHalfPlane g are the g-images of the two canonical sides, Set.range (geodesicLine g)
(via range_geodesicLine) is the g-image of the axis, and the three are pairwise disjoint and
cover ℍ (rightHalfPlane_union_range_geodesicLine_union_leftHalfPlane).
The labelling is not determined by geodesicLine g alone: which side is called right depends
on the chosen representing g, and the two sides are genuinely distinct
(rightHalfPlane_ne_leftHalfPlane). pslS, the element of PSL(2, ℝ) representing z ↦ -1/z,
witnesses this non-canonicity: for g' = g * pslS,
Set.range (geodesicLine g') = Set.range (geodesicLine g) (range_geodesicLine_mul_pslS)
but rightHalfPlane g' = leftHalfPlane g (rightHalfPlane_mul_pslS) — z ↦ -1/z fixes
{z | z.re = 0} setwise and sends 1 + i to -1/2 + i/2. That every pair of representatives
with the same line image gives the same unordered pair of sides is not proved here.
The sides also have an equation. For a representative !![a, b; c, d] of g, the real part of
g⁻¹ • z is a positive multiple of sideForm g z = -(c d) |z|² + (a d + b c) Re z - a b
(exists_pos_re_inv_smul_eq), a quantity unchanged by negating the representative. Hence the
left half-plane of g is {sideForm g < 0}, the geodesic line is {sideForm g = 0} and the
right half-plane is {sideForm g > 0}.
Main declarations #
TauCeti.UpperHalfPlane.rightHalfPlane g,TauCeti.UpperHalfPlane.leftHalfPlane g— the two open half-planes bounded bygeodesicLine g, asg-translates of the canonical pair for the raw imaginary axis;rightHalfPlane_def/leftHalfPlane_defrestate the body.mem_rightHalfPlane_iffandmem_leftHalfPlane_ifftest membership directly, without unfolding the translate;rightHalfPlane_one/leftHalfPlane_oneandsmul_rightHalfPlane/smul_leftHalfPlanegive their value atg = 1and their equivariance, matchingGeodesic.lean's own API for the line.TauCeti.UpperHalfPlane.isOpen_rightHalfPlane,isOpen_leftHalfPlane— both are open.TauCeti.UpperHalfPlane.disjoint_rightHalfPlane_leftHalfPlane,disjoint_rightHalfPlane_range_geodesicLine,disjoint_leftHalfPlane_range_geodesicLine— the three pieces are pairwise disjoint, andTauCeti.UpperHalfPlane.rightHalfPlane_union_range_geodesicLine_union_leftHalfPlanesays they coverℍ.TauCeti.UpperHalfPlane.rightHalfPlane_nonempty,leftHalfPlane_nonempty, andrightHalfPlane_ne_leftHalfPlane— the two half-planes are nonempty and genuinely distinct.TauCeti.UpperHalfPlane.frontier_rightHalfPlane,frontier_leftHalfPlane— the geodesic line is the topological boundary of each half-plane it bounds, viaclosure_rightHalfPlaneandclosure_leftHalfPlane;mem_closure_rightHalfPlane_iff/mem_closure_leftHalfPlane_ifftest membership in the closed half-planes directly.TauCeti.UpperHalfPlane.rightHalfPlane_mul_pslS,leftHalfPlane_mul_pslS— witness thatrightHalfPlane/leftHalfPlanedepend on the chosen representative of a geodesic line, not just its image (TauCeti.pslSis thePSL(2, ℝ)element ofz ↦ -1/z;Geodesic.lean'srange_geodesicLine_mul_pslSis the companion fact for the line itself).TauCeti.UpperHalfPlane.rightHalfPlane_mul_dilation,leftHalfPlane_mul_dilation— by contrast, reparametrising a geodesic line by a dilation (geodesicLine_mul_dilation) changes neither half-plane.TauCeti.UpperHalfPlane.sideForm g: the real quadratic form whose sign is the side ofgeodesicLine g, withsideForm_mkandsideForm_mk_ofRealin the entries of a representative;mem_leftHalfPlane_iff_sideForm_neg,mem_rightHalfPlane_iff_sideForm_pos,mem_range_geodesicLine_iff_sideForm_eq_zero,mem_closure_leftHalfPlane_iff_sideForm_nonpos;sideForm_mul_dilation: it too is unchanged by a dilation;exists_sideForm_eq_mul_normSq_sub: a side form vanishing at two points of a circle centred on the real axis, with distinct real parts, is a multiple of the circle's equation.
The right half-plane bounded by geodesicLine g: the g-translate of the points with
positive real part.
Equations
- TauCeti.UpperHalfPlane.rightHalfPlane g = g • {z : UpperHalfPlane | 0 < z.re}
Instances For
The left half-plane bounded by geodesicLine g: the g-translate of the points with
negative real part.
Equations
- TauCeti.UpperHalfPlane.leftHalfPlane g = g • {z : UpperHalfPlane | z.re < 0}
Instances For
Restatement of the body of rightHalfPlane, unfolded from the def.
Restatement of the body of leftHalfPlane, unfolded from the def.
Membership test for the right half-plane, without unfolding the smul-image.
Membership test for the left half-plane, without unfolding the smul-image.
The right half-plane of the translation by x is {x < re}.
The left half-plane of the translation by x is {re < x}.
The right half-plane of the identity is the canonical {z | 0 < z.re}.
The left half-plane of the identity is the canonical {z | z.re < 0}.
Translating a right half-plane by h gives the right half-plane of h * g.
Translating a left half-plane by h gives the left half-plane of h * g.
The right half-plane bounded by geodesicLine g is open.
The left half-plane bounded by geodesicLine g is open.
The right and left half-planes bounded by the same geodesicLine g are disjoint.
The right half-plane bounded by geodesicLine g is disjoint from the line itself.
The left half-plane bounded by geodesicLine g is disjoint from the line itself.
The right half-plane, the geodesic line, and the left half-plane, all bounded by
geodesicLine g, cover ℍ. With the three disjoint_* lemmas above, every point lies in
exactly one of the three.
The right half-plane is nonempty.
The left half-plane is nonempty.
The right and left half-planes bounded by the same geodesicLine g are genuinely distinct
sets, not merely disjoint.
The closure of the right half-plane adds exactly the geodesic line, its boundary.
The closure of the left half-plane adds exactly the geodesic line, its boundary.
A point z lies in the closed right half-plane of g iff 0 ≤ (g⁻¹ • z).re.
A point z lies in the closed left half-plane of g iff (g⁻¹ • z).re ≤ 0.
The geodesic line is the boundary of the right half-plane it bounds.
The geodesic line is the boundary of the left half-plane it bounds.
The interior of a closed left half-plane is its open half-plane.
The non-canonicity witness #
pslS is the PSL(2, ℝ) element of z ↦ -1/z. Multiplying any
representative g by it fixes the geodesic line's image (range_geodesicLine_mul_pslS in
Geodesic.lean) but swaps which half-plane is called right, so the labelling is a choice of
representative, not an invariant of the line.
Multiplying by pslS swaps the right half-plane into the left one, although the geodesic
line's image is unchanged (range_geodesicLine_mul_pslS).
Multiplying by pslS swaps the left half-plane into the right one.
The interior of a closed right half-plane is its open half-plane.
Reparametrisation by dilations #
Reparametrising a geodesic line by a dilation does not change its right half-plane.
Reparametrising a geodesic line by a dilation does not change its left half-plane.
The side form #
The real quadratic form -(c d) |z|² + (a d + b c) Re z - a b of a representative
!![a, b; c, d] of g, which does not depend on the representative. Its sign on ℍ is the side
of geodesicLine g (mem_leftHalfPlane_iff_sideForm_neg).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real part of g⁻¹ • z is a positive multiple of the side form at z.
The left half-plane of geodesicLine g is where the side form is negative.
The right half-plane of geodesicLine g is where the side form is positive.
The geodesic line of g is the zero set of the side form in ℍ.
The closed left half-plane of geodesicLine g is where the side form is nonpositive.
Reparametrising a geodesic line by a dilation does not change its side form.
A side form vanishing at two points of a circle centred on the real axis, with distinct real parts, is a nonzero multiple of the equation of that circle.