feat(Geometry/Euclidean/Sphere/Tangent): orthRadius-related lemmas (#31731)

Add further lemmas about tangency, the common theme of which is that they relate in some way to `orthRadius` (the full tangent space rather than only a subspace thereof). In particular, give its `finrank` in a finite-dimensional space and describe tangent spaces that have that `finrank`, and, not limited to a finite-dimensional space, the two tangent spaces that are parallel to a given `orthRadius` space.

Author: jsm28

Mathlib/Geometry/Euclidean/Sphere/Tangent.lean

@@ -5,6 +5,7 @@ Authors: Joseph Myers
 -/
 module
 
+public import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
 public import Mathlib.Geometry.Euclidean.Projection
 public import Mathlib.Geometry.Euclidean.Sphere.Basic
 
@@ -58,6 +59,7 @@ namespace EuclideanGeometry
 namespace Sphere
 
 open AffineSubspace RealInnerProductSpace
+open scoped Affine
 
 variable {V P : Type*}
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
@@ -123,6 +125,32 @@ lemma orthRadius_le_orthRadius_iff {s : Sphere P} {p q : P} :
   have hqp := orthRadius_le_orthRadius_iff.1 h.symm.le
   grind
 
+lemma finrank_orthRadius [FiniteDimensional ℝ V] {s : Sphere P} {p : P} (hp : p ≠ s.center) :
+    Module.finrank ℝ (s.orthRadius p).direction + 1 = Module.finrank ℝ V := by
+  rw [orthRadius, add_comm, direction_mk']
+  convert (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal
+  exact (finrank_span_singleton (vsub_ne_zero.2 hp)).symm
+
+lemma orthRadius_map {s : Sphere P} (p : P) {f : P ≃ᵃⁱ[ℝ] P} (h : f s.center = s.center) :
+    (s.orthRadius p).map f.toAffineMap = s.orthRadius (f p) := by
+  rw [orthRadius, map_mk', orthRadius]
+  convert rfl using 2
+  convert (Submodule.map_orthogonal (ℝ ∙ (p -ᵥ s.center)) f.linearIsometryEquiv).symm
+  simp [Submodule.map_span, Set.image_singleton, h]
+
+lemma direction_orthRadius_le_iff {s : Sphere P} {p q : P} :
+    (s.orthRadius p).direction ≤ (s.orthRadius q).direction ↔
+      ∃ r : ℝ, q -ᵥ s.center = r • (p -ᵥ s.center) := by
+  simp [Submodule.orthogonal_le_orthogonal_iff, Submodule.mem_span_singleton, eq_comm]
+
+lemma orthRadius_parallel_orthRadius_iff {s : Sphere P} {p q : P} :
+    s.orthRadius p ∥ s.orthRadius q ↔ ∃ r : ℝ, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center) := by
+  simp only [orthRadius, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, direction_mk',
+    Submodule.orthogonalComplement_eq_orthogonalComplement,
+    Submodule.span_singleton_eq_span_singleton, ← coe_eq_bot_iff,
+    ← Set.not_nonempty_iff_eq_empty, mk'_nonempty, not_true_eq_false, and_true]
+  exact ⟨fun ⟨r, h⟩ ↦ ⟨r, r.ne_zero, h.symm⟩, fun ⟨r, hr, h⟩ ↦ ⟨.mk0 r hr, h.symm⟩⟩
+
 /-- The affine subspace `as` is tangent to the sphere `s` at the point `p`. -/
 structure IsTangentAt (s : Sphere P) (p : P) (as : AffineSubspace ℝ P) : Prop where
   mem_sphere : p ∈ s
@@ -194,6 +222,16 @@ lemma IsTangentAt.dist_eq_of_mem_of_mem {s : Sphere P} {p₁ p₂ q : P}
   have h2 := dist_sq_eq_of_mem h₂ hq_mem₂
   rwa [h1, add_left_cancel_iff, sq_eq_sq₀ dist_nonneg dist_nonneg] at h2
 
+lemma IsTangentAt.eq_orthRadius_of_finrank_add_one_eq {s : Sphere P} {as : AffineSubspace ℝ P}
+    {p : P} (ht : s.IsTangentAt p as) (hr : s.radius ≠ 0)
+    (hfr : Module.finrank ℝ as.direction + 1 = Module.finrank ℝ V) : as = s.orthRadius p := by
+  have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ hfr.symm
+  have hp : p ≠ s.center := fun h ↦ (h ▸ s.center_mem_iff).not.2 hr ht.mem_sphere
+  rw [← finrank_orthRadius hp, Nat.add_right_cancel_iff] at hfr
+  exact eq_of_direction_eq_of_nonempty_of_le
+    (Submodule.eq_of_le_of_finrank_eq (direction_le ht.le_orthRadius) hfr) ⟨p, ht.mem_space⟩
+    ht.le_orthRadius
+
 /-- The affine subspace `as` is tangent to the sphere `s` at some point. -/
 def IsTangent (s : Sphere P) (as : AffineSubspace ℝ P) : Prop :=
   ∃ p, s.IsTangentAt p as
@@ -267,6 +305,40 @@ lemma isTangent_iff_isTangentAt_orthogonalProjection {s : Sphere P} {as : Affine
 
 alias ⟨IsTangent.isTangentAt, _⟩ := isTangent_iff_isTangentAt_orthogonalProjection
 
+lemma IsTangent.eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius {s : Sphere P}
+    {as : AffineSubspace ℝ P} {p : P} (h : s.IsTangent as) (hpar : as ∥ s.orthRadius p)
+    (hp : p ∈ s) :
+    as = s.orthRadius p ∨ as = s.orthRadius (Equiv.pointReflection s.center p) := by
+  rcases h with ⟨q, hqs, hqas, hqo⟩
+  have hd := direction_le hqo
+  rw [hpar.direction_eq, direction_orthRadius_le_iff] at hd
+  obtain ⟨r, hr⟩ := hd
+  rcases eq_or_ne s.radius 0 with hrad | hrad
+  · rw [mem_sphere, hrad, dist_eq_zero] at hp hqs
+    rw [hp, orthRadius_center] at hpar ⊢
+    rw [hqs, orthRadius_center] at hqo
+    exact .inl (eq_of_direction_eq_of_nonempty_of_le hpar.direction_eq ⟨q, hqas⟩ hqo)
+  obtain rfl : as = s.orthRadius q := by
+    refine eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo
+    rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]
+    congr 1
+    rcases eq_or_ne r 0 with rfl | hr0
+    · simp_all
+    · rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]
+  rcases eq_or_ne r 0 with rfl | hr0
+  · simp_all
+  · have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖ := by
+      rw [hr]
+    simp_rw [norm_smul, Real.norm_eq_abs, ← dist_eq_norm_vsub, mem_sphere.1 hp,
+      mem_sphere.1 hqs, right_eq_mul₀ hrad] at hr'
+    rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl
+    · simp_all
+    · right
+      convert rfl
+      rw [← eq_vadd_iff_vsub_eq] at hr
+      rw [hr]
+      simp [Equiv.pointReflection_apply]
+
 lemma IsTangentAt.eq_orthogonalProjection {s : Sphere P} {p : P} {as : AffineSubspace ℝ P}
     [Nonempty as] [as.direction.HasOrthogonalProjection] (h : s.IsTangentAt p as) :
     p = orthogonalProjection as s.center := by