refactor(geometry/euclidean/basic): adjust Euclidean geometry to use affine isometries for reflections (#8662)

Author: hrmacbeth

src/analysis/normed_space/inner_product.lean

@@ -1087,6 +1087,14 @@ begin
     linarith }
 end
 
+/-- Given two orthogonal vectors, their sum and difference have equal norms. -/
+lemma norm_sub_eq_norm_add {v w : E} (h : ⟪v, w⟫ = 0) : ∥w - v∥ = ∥w + v∥ :=
+begin
+  rw ←mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _),
+  simp [h, ←inner_self_eq_norm_sq, inner_add_left, inner_add_right, inner_sub_left,
+    inner_sub_right, inner_re_symm]
+end
+
 /-- The real inner product of two vectors, divided by the product of their
 norms, has absolute value at most 1. -/
 lemma abs_real_inner_div_norm_mul_norm_le_one (x y : F) : absR (⟪x, y⟫_ℝ / (∥x∥ * ∥y∥)) ≤ 1 :=
@@ -2255,6 +2263,49 @@ by { rw ← smul_orthogonal_projection_singleton 𝕜 w, simp [hv] }
 
 end orthogonal_projection
 
+section reflection
+variables {𝕜} (K) [complete_space K]
+
+/-- Reflection in a complete subspace of an inner product space.  The word "reflection" is
+sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes
+more generally to cover operations such as reflection in a point.  The definition here, of
+reflection in a subspace, is a more general sense of the word that includes both those common
+cases. -/
+def reflection : E ≃ₗᵢ[𝕜] E :=
+{ norm_map' := begin
+    intros x,
+    let w : K := orthogonal_projection K x,
+    let v := x - w,
+    have : ⟪v, w⟫ = 0 := orthogonal_projection_inner_eq_zero x w w.2,
+    convert norm_sub_eq_norm_add this using 2,
+    { simp [bit0],
+      dsimp [w, v],
+      abel },
+    { simp [bit0] }
+  end,
+  ..linear_equiv.of_involutive
+      (bit0 (K.subtype.comp (orthogonal_projection K).to_linear_map) - linear_map.id)
+      (λ x, by simp [bit0]) }
+
+variables {K}
+
+/-- The result of reflecting. -/
+lemma reflection_apply (p : E) : reflection K p = bit0 ↑(orthogonal_projection K p) - p := rfl
+
+/-- Reflection is its own inverse. -/
+@[simp] lemma reflection_symm : (reflection K).symm = reflection K := rfl
+
+variables (K)
+
+/-- Reflecting twice in the same subspace. -/
+@[simp] lemma reflection_reflection (p : E) : reflection K (reflection K p) = p :=
+(reflection K).left_inv p
+
+/-- Reflection is involutive. -/
+lemma reflection_involutive : function.involutive (reflection K) := reflection_reflection K
+
+end reflection
+
 /-- The subspace of vectors orthogonal to a given subspace. -/
 def submodule.orthogonal : submodule 𝕜 E :=
 { carrier := {v | ∀ u ∈ K, ⟪u, v⟫ = 0},

src/geometry/euclidean/basic.lean

@@ -5,7 +5,7 @@ Authors: Joseph Myers, Manuel Candales
 -/
 import analysis.special_functions.trigonometric
 import algebra.quadratic_discriminant
-import analysis.normed_space.add_torsor
+import analysis.normed_space.affine_isometry
 import data.matrix.notation
 import linear_algebra.affine_space.finite_dimensional
 import tactic.fin_cases
@@ -864,6 +864,15 @@ begin
     exact hp }
 end
 
+@[simp] lemma orthogonal_projection_mem_subspace_eq_self {s : affine_subspace ℝ P} [nonempty s]
+  [complete_space s.direction] (p : s) :
+  orthogonal_projection s p = p :=
+begin
+  ext,
+  rw orthogonal_projection_eq_self_iff,
+  exact p.2
+end
+
 /-- Orthogonal projection is idempotent. -/
 @[simp] lemma orthogonal_projection_orthogonal_projection (s : affine_subspace ℝ P) [nonempty s]
   [complete_space s.direction] (p : P) :
@@ -911,6 +920,18 @@ lemma vsub_orthogonal_projection_mem_direction_orthogonal (s : affine_subspace 
 direction_mk' p s.directionᗮ ▸
   vsub_mem_direction (self_mem_mk' _ _) (orthogonal_projection_mem_orthogonal s p)
 
+/-- Subtracting the `orthogonal_projection` from `p` produces a result in the kernel of the linear
+part of the orthogonal projection. -/
+lemma orthogonal_projection_vsub_orthogonal_projection (s : affine_subspace ℝ P) [nonempty s]
+  [complete_space s.direction] (p : P) :
+  _root_.orthogonal_projection s.direction (p -ᵥ orthogonal_projection s p) = 0 :=
+begin
+  apply orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero,
+  intros c hc,
+  rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
+    (orthogonal_projection_vsub_mem_direction_orthogonal s p c hc), neg_zero]
+end
+
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector was
 in the orthogonal direction. -/
@@ -981,42 +1002,27 @@ and complete.  The word "reflection" is sometimes understood to mean
 specifically reflection in a codimension-one subspace, and sometimes
 more generally to cover operations such as reflection in a point.  The
 definition here, of reflection in an affine subspace, is a more
-general sense of the word that includes both those common cases.  If
-the subspace is empty or not complete, `orthogonal_projection` is
-defined as the identity map, which results in `reflection` being the
-identity map in that case as well. -/
+general sense of the word that includes both those common cases. -/
 def reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
-  P ≃ᵢ P :=
-{ to_fun := λ p, (↑(orthogonal_projection s p) -ᵥ p) +ᵥ orthogonal_projection s p,
-  inv_fun := λ p, (↑(orthogonal_projection s p) -ᵥ p) +ᵥ orthogonal_projection s p,
-  left_inv := λ p, by simp [vsub_vadd_eq_vsub_sub, -orthogonal_projection_linear],
-  right_inv := λ p, by simp [vsub_vadd_eq_vsub_sub, -orthogonal_projection_linear],
-  isometry_to_fun := begin
-    dsimp only,
-    rw isometry_emetric_iff_metric,
-    intros p₁ p₂,
-    rw [←mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_eq_norm_vsub V
-          ((↑(orthogonal_projection s p₁) -ᵥ p₁) +ᵥ ↑(orthogonal_projection s p₁)),
-        dist_eq_norm_vsub V p₁, ←inner_self_eq_norm_sq, ←inner_self_eq_norm_sq],
-    calc
-      ⟪((orthogonal_projection s p₁ : P) -ᵥ p₁ +ᵥ (orthogonal_projection s p₁ : P) -ᵥ
-      ((orthogonal_projection s p₂ : P) -ᵥ p₂ +ᵥ orthogonal_projection s p₂)),
-      ((orthogonal_projection s p₁ : P) -ᵥ p₁ +ᵥ (orthogonal_projection s p₁ : P) -ᵥ
-      ((orthogonal_projection s p₂ : P) -ᵥ p₂ +ᵥ orthogonal_projection s p₂))⟫
-        = ⟪(_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂)) +
-          _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) - (p₁ -ᵥ p₂),
-          _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) +
-          _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) - (p₁ -ᵥ p₂)⟫
-        : by { rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
-          ←vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub, ←add_sub_assoc, ←coe_vsub,
-          ←affine_map.linear_map_vsub], simp }
-    ... = -4 * inner (p₁ -ᵥ p₂ - (_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) : V))
-                   (_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂)) +
-          ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫
-        : by { simp [inner_sub_left, inner_sub_right, inner_add_left, inner_add_right,
-                 real_inner_comm (p₁ -ᵥ p₂)], ring }
-    ... = ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ : by simp,
-  end }
+  P ≃ᵃⁱ[ℝ] P :=
+affine_isometry_equiv.mk'
+  (λ p, (↑(orthogonal_projection s p) -ᵥ p) +ᵥ orthogonal_projection s p)
+  (_root_.reflection s.direction)
+  ↑(classical.arbitrary s)
+  begin
+    intros p,
+    let v := p -ᵥ ↑(classical.arbitrary s),
+    let a : V := _root_.orthogonal_projection s.direction v,
+    let b : P := ↑(classical.arbitrary s),
+    have key : a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b),
+    { rw [← add_vadd, vsub_vadd_eq_vsub_sub, vsub_vadd, vadd_vsub],
+      congr' 1,
+      abel },
+    have : p = v +ᵥ ↑(classical.arbitrary s) := (vsub_vadd p ↑(classical.arbitrary s)).symm,
+    simpa only [coe_vadd, reflection_apply, affine_map.map_vadd, orthogonal_projection_linear,
+      orthogonal_projection_mem_subspace_eq_self, vadd_vsub, continuous_linear_map.coe_coe,
+      continuous_linear_equiv.coe_coe, this] using key,
+  end
 
 /-- The result of reflecting. -/
 lemma reflection_apply (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] (p : P) :
@@ -1028,16 +1034,25 @@ lemma eq_reflection_of_eq_subspace {s s' : affine_subspace ℝ P} [nonempty s]
   (reflection s p : P) = (reflection s' p : P) :=
 by unfreezingI { subst h }
 
-/-- Reflection is its own inverse. -/
-@[simp] lemma reflection_symm (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
-  (reflection s).symm = reflection s :=
-rfl
-
 /-- Reflecting twice in the same subspace. -/
 @[simp] lemma reflection_reflection (s : affine_subspace ℝ P) [nonempty s]
   [complete_space s.direction] (p : P) :
   reflection s (reflection s p) = p :=
-(reflection s).left_inv p
+begin
+  have : ∀ a : s, ∀ b : V, (_root_.orthogonal_projection s.direction) b = 0
+    → reflection s (reflection s (b +ᵥ a)) = b +ᵥ a,
+  { intros a b h,
+    have : (a:P) -ᵥ (b +ᵥ a) = - b,
+    { rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub] },
+    simp [reflection, h, this] },
+  rw ← vsub_vadd p (orthogonal_projection s p),
+  exact this (orthogonal_projection s p) _ (orthogonal_projection_vsub_orthogonal_projection s p),
+end
+
+/-- Reflection is its own inverse. -/
+@[simp] lemma reflection_symm (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
+  (reflection s).symm = reflection s :=
+by { ext, rw ← (reflection s).injective.eq_iff, simp }
 
 /-- Reflection is involutive. -/
 lemma reflection_involutive (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
@@ -1088,7 +1103,7 @@ lemma dist_reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s
   dist p₁ (reflection s p₂) = dist (reflection s p₁) p₂ :=
 begin
   conv_lhs { rw ←reflection_reflection s p₁ },
-  exact (reflection s).dist_eq _ _
+  exact (reflection s).dist_map _ _
 end
 
 /-- A point in the subspace is equidistant from another point and its
@@ -1098,7 +1113,7 @@ lemma dist_reflection_eq_of_mem (s : affine_subspace ℝ P) [nonempty s] [comple
   dist p₁ (reflection s p₂) = dist p₁ p₂ :=
 begin
   rw ←reflection_eq_self_iff p₁ at hp₁,
-  convert (reflection s).dist_eq p₁ p₂,
+  convert (reflection s).dist_map p₁ p₂,
   rw hp₁
 end
 

src/geometry/euclidean/circumcenter.lean

@@ -642,8 +642,9 @@ begin
     = ↑(orthogonal_projection (affine_span ℝ (set.range (s.face hc).points)) s.circumcenter),
   { apply eq_orthogonal_projection_of_eq_subspace,
     simp },
-  rw [reflection_apply, h_faces, s.orthogonal_projection_circumcenter hc, circumcenter_eq_centroid,
-      s.face_centroid_eq_centroid hc, centroid_eq_affine_combination_of_points_with_circumcenter,
+  rw [euclidean_geometry.reflection_apply, h_faces, s.orthogonal_projection_circumcenter hc,
+      circumcenter_eq_centroid, s.face_centroid_eq_centroid hc,
+      centroid_eq_affine_combination_of_points_with_circumcenter,
       circumcenter_eq_affine_combination_of_points_with_circumcenter, ←@vsub_eq_zero_iff_eq V,
       affine_combination_vsub, weighted_vsub_vadd_affine_combination, affine_combination_vsub,
       weighted_vsub_apply, sum_points_with_circumcenter],