feat(Geometry/Euclidean/Angle): the unoriented angle at the center in terms of the angle at the circumference

Author: Scarlett-le

Mathlib/Geometry/Euclidean/Angle/Sphere.lean

@@ -179,6 +179,46 @@ theorem oangle_center_eq_two_zsmul_oangle {s : Sphere P} {p₁ p₂ p₃ : P} (h
   rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃] <;>
     simp [hp₂p₁, hp₂p₃]
 
+/-- The angle at the center of a circle equals twice the angle at the circumference, unoriented
+angle version, provided twice the angle at the circumference is at most `π`. -/
+theorem angle_center_eq_two_mul_angle_of_two_mul_angle_le_pi {s : Sphere P} {p₁ p₂ p₃ : P}
+    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃)
+    (h : 2 * ∠ p₁ p₂ p₃ ≤ π) : ∠ p₁ s.center p₃ = 2 * ∠ p₁ p₂ p₃ := by
+  have hp₁c : p₁ ≠ s.center := by
+    rintro rfl
+    rw [center_mem_iff] at hp₁
+    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
+  have hp₃c : p₃ ≠ s.center := by
+    rintro rfl
+    rw [center_mem_iff] at hp₃
+    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
+    ⟨mul_nonneg zero_le_two (angle_nonneg p₁ p₂ p₃), h⟩ ?_
+  rw [← cos_oangle_eq_cos_angle hp₁c hp₃c,
+    oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃, Real.cos_two_mul,
+    ← cos_oangle_eq_cos_angle hp₂p₁.symm hp₂p₃.symm, two_zsmul, Real.Angle.cos_add]
+  nlinarith [Real.Angle.cos_sq_add_sin_sq (∡ p₁ p₂ p₃)]
+
+/-- The angle at the center of a circle is `2 * π` minus twice the angle at the circumference,
+unoriented angle version, provided twice the angle at the circumference is at least `π`. -/
+theorem angle_center_eq_two_pi_sub_two_mul_angle_of_pi_le_two_mul_angle {s : Sphere P}
+    {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁)
+    (hp₂p₃ : p₂ ≠ p₃) (h : π ≤ 2 * ∠ p₁ p₂ p₃) :
+    ∠ p₁ s.center p₃ = 2 * π - 2 * ∠ p₁ p₂ p₃ := by
+  have hp₁c : p₁ ≠ s.center := by
+    rintro rfl; rw [center_mem_iff] at hp₁
+    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
+  have hp₃c : p₃ ≠ s.center := by
+    rintro rfl; rw [center_mem_iff] at hp₃
+    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
+    ⟨by linarith [angle_le_pi p₁ p₂ p₃], by linarith⟩ ?_
+  rw [show (2 : ℝ) * π - 2 * ∠ p₁ p₂ p₃ = -(2 * ∠ p₁ p₂ p₃) + 2 * π by ring,
+    Real.cos_add_two_pi, Real.cos_neg, ← cos_oangle_eq_cos_angle hp₁c hp₃c,
+    oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃, Real.cos_two_mul,
+    ← cos_oangle_eq_cos_angle hp₂p₁.symm hp₂p₃.symm, two_zsmul, Real.Angle.cos_add]
+  nlinarith [Real.Angle.cos_sq_add_sin_sq (∡ p₁ p₂ p₃)]
+
 /-- Oriented angle version of "angles in same segment are equal" and "opposite angles of a
 cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result),
 represented here as equality of twice the angles. -/