feat(analysis/normed_space/inner_product): reflections API (#8884)

Reflections, as isometries of an inner product space, were defined in #8660.  In this PR, various elementary lemmas filling out the API:

- Lemmas about reflection through a subspace K, of a point which is in (i) K itself; (ii) the orthogonal complement of K.

- Lemmas relating the orthogonal projection/reflection on the `submodule.map` of a subspace, with the orthogonal projection/reflection on the original subspace.

- Lemma characterizing the reflection in the trivial subspace.



Co-authored-by: Scott Morrison <scott@tqft.net>

src/analysis/normed_space/inner_product.lean

@@ -2211,6 +2211,32 @@ end
 @[simp] lemma orthogonal_projection_mem_subspace_eq_self (v : K) : orthogonal_projection K v = v :=
 by { ext, apply eq_orthogonal_projection_of_mem_of_inner_eq_zero; simp }
 
+/-- A point equals its orthogonal projection if and only if it lies in the subspace. -/
+lemma orthogonal_projection_eq_self_iff {v : E} :
+  (orthogonal_projection K v : E) = v ↔ v ∈ K :=
+begin
+  refine ⟨λ h, _, λ h, eq_orthogonal_projection_of_mem_of_inner_eq_zero h _⟩,
+  { rw ← h,
+    simp },
+  { simp }
+end
+
+/-- Orthogonal projection onto the `submodule.map` of a subspace. -/
+lemma orthogonal_projection_map_apply {E E' : Type*} [inner_product_space 𝕜 E]
+  [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [finite_dimensional 𝕜 p]
+  (x : E') :
+  (orthogonal_projection (p.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x : E')
+  = f (orthogonal_projection p (f.symm x)) :=
+begin
+  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
+  { exact ⟨orthogonal_projection p (f.symm x), submodule.coe_mem _, by simp⟩, },
+  rintros w ⟨a, ha, rfl⟩,
+  suffices : inner (f (f.symm x - orthogonal_projection p (f.symm x))) (f a) = (0:𝕜),
+  { simpa using this },
+  rw f.inner_map_map,
+  exact orthogonal_projection_inner_eq_zero _ _ ha,
+end
+
 /-- The orthogonal projection onto the trivial submodule is the zero map. -/
 @[simp] lemma orthogonal_projection_bot : orthogonal_projection (⊥ : submodule 𝕜 E) = 0 :=
 by ext
@@ -2302,6 +2328,36 @@ variables (K)
 /-- Reflection is involutive. -/
 lemma reflection_involutive : function.involutive (reflection K) := reflection_reflection K
 
+variables {K}
+
+/-- A point is its own reflection if and only if it is in the subspace. -/
+lemma reflection_eq_self_iff (x : E) : reflection K x = x ↔ x ∈ K :=
+begin
+  rw [←orthogonal_projection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
+    ← two_smul' 𝕜],
+  refine (smul_right_injective E _).eq_iff,
+  exact two_ne_zero
+end
+
+lemma reflection_mem_subspace_eq_self {x : E} (hx : x ∈ K) : reflection K x = x :=
+(reflection_eq_self_iff x).mpr hx
+
+/-- Reflection in the `submodule.map` of a subspace. -/
+lemma reflection_map_apply {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] (x : E') :
+  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x = f (reflection K (f.symm x)) :=
+by simp [bit0, reflection_apply, orthogonal_projection_map_apply f K x]
+
+/-- Reflection in the `submodule.map` of a subspace. -/
+lemma reflection_map {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] :
+  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) = f.symm.trans ((reflection K).trans f) :=
+linear_isometry_equiv.ext $ reflection_map_apply f K
+
+/-- Reflection through the trivial subspace {0} is just negation. -/
+@[simp] lemma reflection_bot : reflection (⊥ : submodule 𝕜 E) = linear_isometry_equiv.neg 𝕜 :=
+by ext; simp [reflection_apply]
+
 end reflection
 
 /-- The subspace of vectors orthogonal to a given subspace. -/
@@ -2540,18 +2596,35 @@ lemma orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero
   orthogonal_projection K v = 0 :=
 by { ext, convert eq_orthogonal_projection_of_mem_orthogonal _ _; simp [hv] }
 
+/-- The reflection in `K` of an element of `Kᗮ` is its negation. -/
+lemma reflection_mem_subspace_orthogonal_complement_eq_neg
+  [complete_space K] {v : E} (hv : v ∈ Kᗮ) :
+  reflection K v = - v :=
+by simp [reflection_apply, orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero hv]
+
 /-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero. -/
 lemma orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
   [complete_space E] {v : E} (hv : v ∈ K) :
   orthogonal_projection Kᗮ v = 0 :=
 orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero (K.le_orthogonal_orthogonal hv)
 
+/-- The reflection in `Kᗮ` of an element of `K` is its negation. -/
+lemma reflection_mem_subspace_orthogonal_precomplement_eq_neg
+  [complete_space E] {v : E} (hv : v ∈ K) :
+  reflection Kᗮ v = -v :=
+reflection_mem_subspace_orthogonal_complement_eq_neg (K.le_orthogonal_orthogonal hv)
+
 /-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/
 lemma orthogonal_projection_orthogonal_complement_singleton_eq_zero [complete_space E] (v : E) :
   orthogonal_projection (𝕜 ∙ v)ᗮ v = 0 :=
 orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
   (submodule.mem_span_singleton_self v)
 
+/-- The reflection in `(𝕜 ∙ v)ᗮ` of `v` is `-v`. -/
+lemma reflection_orthogonal_complement_singleton_eq_neg [complete_space E] (v : E) :
+  reflection (𝕜 ∙ v)ᗮ v = -v :=
+reflection_mem_subspace_orthogonal_precomplement_eq_neg (submodule.mem_span_singleton_self v)
+
 variables (K)
 
 /-- In a complete space `E`, a vector splits as the sum of its orthogonal projections onto a