The oriented angle between two geodesics and the side of a line

UpperHalfPlane.orientedAngle A B C is the oriented angle at A from the geodesic towards B to the geodesic towards C, the oriented angle (Orientation.oangle for the standard orientation of ℂ) between the two velocities at A. Its absolute value is the unoriented UpperHalfPlane.interiorAngle A B C (UpperHalfPlane.interiorAngle_eq_abs_toReal_orientedAngle), it is invariant under PSL(2, ℝ) when A ≠ B and A ≠ C (orientedAngle_smul), and it is additive (UpperHalfPlane.orientedAngle_add). For A ≠ C, its sign is the side of the line through A and B on which C lies: +1 on the left, -1 on the right, 0 on the line (orientedAngle_sign_eq_one_iff and companions); in particular the angles of a nondegenerate triangle lie strictly between 0 and π (interiorAngle_pos, interiorAngle_lt_pi). Three consequences used for polygons: orientation is cyclically invariant (mem_leftHalfPlane_geodesicBetween_of_mem_leftHalfPlane: if C is left of A → B then A is left of B → C), unoriented angles add when the middle geodesic lies between the outer two (interiorAngle_add), and the angular order of two points on the left of A → B is read off the side of the geodesic through the first (toReal_orientedAngle_lt_iff).

Source: Katok, Fuchsian groups, geodesic flows…, Clay Math. Proc. 10 (2010), Corollary 5.2 p. 18 (Möbius transformations preserve angles and orientation). The sign–side correspondence and the cyclic invariance are not stated in the sources.

The oriented angle

noncomputable def UpperHalfPlane.orientedAngle (A B C : UpperHalfPlane) : Real.Angle

The oriented angle at A from the geodesic towards B to the geodesic towards C.

Equations

• One or more equations did not get rendered due to their size.

theorem UpperHalfPlane.orientedAngle_def (A B C : UpperHalfPlane) : A.orientedAngle B C = Complex.orientation.oangle (TauCeti.UpperHalfPlane.velocity (TauCeti.UpperHalfPlane.geodesicBetween A B) 0) (TauCeti.UpperHalfPlane.velocity (TauCeti.UpperHalfPlane.geodesicBetween A C) 0)

orientedAngle is the oriented angle between the velocities at parameter 0.

theorem UpperHalfPlane.interiorAngle_eq_abs_toReal_orientedAngle (A B C : UpperHalfPlane) : A.interiorAngle B C = |(A.orientedAngle B C).toReal|

The unoriented angle is the absolute value of the oriented one.

theorem UpperHalfPlane.orientedAngle_rev (A B C : UpperHalfPlane) : A.orientedAngle C B = -A.orientedAngle B C

Reversing the two geodesics negates the oriented angle.

@[simp]

theorem UpperHalfPlane.orientedAngle_self (A B : UpperHalfPlane) : A.orientedAngle B B = 0

The oriented angle of a geodesic with itself is 0.

theorem UpperHalfPlane.orientedAngle_add (A B C D : UpperHalfPlane) : A.orientedAngle B C + A.orientedAngle C D = A.orientedAngle B D

Oriented angles at a common vertex add.

The normal form: the geodesic from A to B as the imaginary axis

theorem UpperHalfPlane.inv_geodesicBetween_smul_left (A B : UpperHalfPlane) : (TauCeti.UpperHalfPlane.geodesicBetween A B)⁻¹ • A = I

The inverse of the geodesic line from A to B moves A to I.

theorem UpperHalfPlane.inv_geodesicBetween_smul_right (A B : UpperHalfPlane) : (TauCeti.UpperHalfPlane.geodesicBetween A B)⁻¹ • B = TauCeti.UpperHalfPlane.geodesicLine 1 (dist A B)

The inverse of the geodesic line from A to B moves B up the imaginary axis, to the point at distance dist A B from I.

theorem UpperHalfPlane.exists_ne_and_geodesicBetween_eq (A B : UpperHalfPlane) : ∃ (B' : UpperHalfPlane), A ≠ B' ∧ TauCeti.UpperHalfPlane.geodesicBetween A B' = TauCeti.UpperHalfPlane.geodesicBetween A B

The geodesic line from A to B is also the line from A to some point B' ≠ A on it; this lets results assuming A ≠ B apply to geodesicBetween A A as well.

Invariance of the oriented angle

theorem TauCeti.UpperHalfPlane.orientedAngle_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {A B C : UpperHalfPlane} (hAB : A ≠ B) (hAC : A ≠ C) : (h • A).orientedAngle (h • B) (h • C) = A.orientedAngle B C

Möbius transformations preserve oriented angles at A, for A ≠ B and A ≠ C. Source: Katok, Fuchsian groups, geodesic flows… (Clay Math. Proc. 10), Corollary 5.2 p. 18.

The normal form: rotations of the imaginary axis

theorem TauCeti.UpperHalfPlane.geodesicBetween_I_geodesicLine_rotation {t : ℝ} (ht : 0 < t) (θ : ℝ) : geodesicBetween UpperHalfPlane.I (geodesicLine (↑(Matrix.SpecialLinearGroup.rotation θ)) t) = ↑(Matrix.SpecialLinearGroup.rotation θ)

The geodesic line from I to a point at positive parameter on the imaginary axis rotated by θ is that rotated axis (compare geodesicBetween_I_geodesicLine_one).

theorem TauCeti.UpperHalfPlane.orientedAngle_I_geodesicLine_one_rotation {d t : ℝ} (hd : 0 < d) (ht : 0 < t) (θ : ℝ) : UpperHalfPlane.I.orientedAngle (geodesicLine 1 d) (geodesicLine (↑(Matrix.SpecialLinearGroup.rotation θ)) t) = ↑(2 * θ)

The oriented angle at I from the geodesic towards the point geodesicLine 1 d of the imaginary axis to the geodesic towards the point geodesicLine (rotation θ) t of its rotation by θ is 2θ, for 0 < d and 0 < t.

The sign of the oriented angle is the side of the line

theorem TauCeti.UpperHalfPlane.orientedAngle_sign_eq_one_iff {A B C : UpperHalfPlane} (hAC : A ≠ C) : (A.orientedAngle B C).sign = 1 ↔ C ∈ leftHalfPlane (geodesicBetween A B)

For A ≠ C, the sign of the oriented angle is +1 exactly when C lies to the left of the geodesic from A to B.

theorem TauCeti.UpperHalfPlane.orientedAngle_sign_eq_neg_one_iff {A B C : UpperHalfPlane} (hAC : A ≠ C) : (A.orientedAngle B C).sign = -1 ↔ C ∈ rightHalfPlane (geodesicBetween A B)

For A ≠ C, the sign of the oriented angle is -1 exactly when C lies to the right of the geodesic from A to B.

theorem TauCeti.UpperHalfPlane.orientedAngle_sign_eq_zero_iff {A B C : UpperHalfPlane} (hAC : A ≠ C) : (A.orientedAngle B C).sign = 0 ↔ C ∈ Set.range (geodesicLine (geodesicBetween A B))

For A ≠ C, the sign of the oriented angle is 0 exactly when C lies on the geodesic through A and B.

theorem TauCeti.UpperHalfPlane.interiorAngle_pos {A B C : UpperHalfPlane} (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) : 0 < A.interiorAngle B C

The angle at A of a nondegenerate triangle is strictly positive.

theorem TauCeti.UpperHalfPlane.interiorAngle_lt_pi {A B C : UpperHalfPlane} (hC : C ∉ Set.range (geodesicLine (geodesicBetween A B))) : A.interiorAngle B C < Real.pi

The angle at A of a nondegenerate triangle is strictly less than π.

Reversal and cyclic invariance of the sides

theorem TauCeti.UpperHalfPlane.leftHalfPlane_geodesicBetween_swap {z w : UpperHalfPlane} (hzw : z ≠ w) : leftHalfPlane (geodesicBetween w z) = rightHalfPlane (geodesicBetween z w)

Reversing the direction of the geodesic through two distinct points swaps its two half-planes.

theorem TauCeti.UpperHalfPlane.rightHalfPlane_geodesicBetween_swap {z w : UpperHalfPlane} (hzw : z ≠ w) : rightHalfPlane (geodesicBetween w z) = leftHalfPlane (geodesicBetween z w)

Reversing the direction of the geodesic through two distinct points swaps its two half-planes.

theorem TauCeti.UpperHalfPlane.notMem_range_geodesicLine_of_mem_leftHalfPlane {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : z ∈ leftHalfPlane g) : z ∉ Set.range (geodesicLine g)

A point of an open left half-plane is not on the bounding line.

theorem TauCeti.UpperHalfPlane.mem_leftHalfPlane_geodesicBetween_of_mem_leftHalfPlane {A B C : UpperHalfPlane} (hAB : A ≠ B) (h : C ∈ leftHalfPlane (geodesicBetween A B)) : A ∈ leftHalfPlane (geodesicBetween B C)

Orientation is cyclically invariant: for A ≠ B, if C lies to the left of the geodesic from A to B, then A lies to the left of the geodesic from B to C.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_geodesicBetween_of_mem_rightHalfPlane {A B C : UpperHalfPlane} (hAB : A ≠ B) (h : C ∈ rightHalfPlane (geodesicBetween A B)) : A ∈ rightHalfPlane (geodesicBetween B C)

Orientation is cyclically invariant: for A ≠ B, if C lies to the right of the geodesic from A to B, then A lies to the right of the geodesic from B to C.

Additivity of unoriented angles and the angular order

theorem TauCeti.UpperHalfPlane.interiorAngle_add {A B C D : UpperHalfPlane} (hC : C ∈ leftHalfPlane (geodesicBetween A B)) (hD : D ∈ leftHalfPlane (geodesicBetween A B)) (hCD : D ∈ leftHalfPlane (geodesicBetween A C)) : A.interiorAngle B D = A.interiorAngle B C + A.interiorAngle C D

Angles add: if C and D lie to the left of the geodesic from A to B, and D lies to the left of the geodesic from A to C, then the angle at A between B and D is the sum of the angles between B and C and between C and D.

theorem TauCeti.UpperHalfPlane.toReal_orientedAngle_lt_iff {A B C D : UpperHalfPlane} (hC : C ∈ leftHalfPlane (geodesicBetween A B)) (hD : D ∈ leftHalfPlane (geodesicBetween A B)) : (A.orientedAngle B C).toReal < (A.orientedAngle B D).toReal ↔ D ∈ leftHalfPlane (geodesicBetween A C)

The angular order of two points to the left of a geodesic is read off the side of the geodesic through the first.