feat(analysis/normed_space/inner_product): upgrade orthogonal project…

…ion to a continuous linear map (#5543) Upgrade the orthogonal projection, from a linear map `E →ₗ[𝕜] K` to a continuous linear map `E →L[𝕜] K`.
leanprover-community · Jan 2, 2021 · ea3815f · ea3815f
1 parent b57d562
commit ea3815f
Show file tree

Hide file tree

Showing 2 changed files with 49 additions and 25 deletions.
diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
@@ -1577,33 +1577,52 @@ begin
   rwa sub_sub_sub_cancel_left at houv
 end
 
+lemma orthogonal_projection_fn_norm_sq (K : submodule 𝕜 E) [complete_space K] (v : E) :
+  ∥v∥ * ∥v∥ = ∥v - (orthogonal_projection_fn K v)∥ * ∥v - (orthogonal_projection_fn K v)∥
+            + ∥orthogonal_projection_fn K v∥ * ∥orthogonal_projection_fn K v∥ :=
+begin
+  set p := orthogonal_projection_fn K v,
+  have h' : ⟪v - p, p⟫ = 0,
+  { exact orthogonal_projection_fn_inner_eq_zero _ _ (orthogonal_projection_fn_mem v) },
+  convert norm_add_square_eq_norm_square_add_norm_square_of_inner_eq_zero (v - p) p h' using 2;
+  simp,
+end
+
 /-- The orthogonal projection onto a complete subspace. -/
-def orthogonal_projection (K : submodule 𝕜 E) [complete_space K] : E →ₗ[𝕜] K :=
-{ to_fun := λ v, ⟨orthogonal_projection_fn K v, orthogonal_projection_fn_mem v⟩,
-  map_add' := λ x y, begin
-    have hm : orthogonal_projection_fn K x + orthogonal_projection_fn K y ∈ K :=
-      submodule.add_mem K (orthogonal_projection_fn_mem x) (orthogonal_projection_fn_mem y),
-    have ho :
-      ∀ w ∈ K, ⟪x + y - (orthogonal_projection_fn K x + orthogonal_projection_fn K y), w⟫ = 0,
-    { intros w hw,
-      rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero _ w hw,
-          orthogonal_projection_fn_inner_eq_zero _ w hw, add_zero] },
-    ext,
-    simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
-  end,
-  map_smul' := λ c x, begin
-    have hm : c • orthogonal_projection_fn K x ∈ K :=
-      submodule.smul_mem K _ (orthogonal_projection_fn_mem x),
-    have ho : ∀ w ∈ K, ⟪c • x - c • orthogonal_projection_fn K x, w⟫ = 0,
-    { intros w hw,
-      rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero _ w hw, mul_zero] },
-    ext,
-    simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
-  end }
+def orthogonal_projection (K : submodule 𝕜 E) [complete_space K] : E →L[𝕜] K :=
+linear_map.mk_continuous
+  { to_fun := λ v, ⟨orthogonal_projection_fn K v, orthogonal_projection_fn_mem v⟩,
+    map_add' := λ x y, begin
+      have hm : orthogonal_projection_fn K x + orthogonal_projection_fn K y ∈ K :=
+        submodule.add_mem K (orthogonal_projection_fn_mem x) (orthogonal_projection_fn_mem y),
+      have ho :
+        ∀ w ∈ K, ⟪x + y - (orthogonal_projection_fn K x + orthogonal_projection_fn K y), w⟫ = 0,
+      { intros w hw,
+        rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero _ w hw,
+            orthogonal_projection_fn_inner_eq_zero _ w hw, add_zero] },
+      ext,
+      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
+    end,
+    map_smul' := λ c x, begin
+      have hm : c • orthogonal_projection_fn K x ∈ K :=
+        submodule.smul_mem K _ (orthogonal_projection_fn_mem x),
+      have ho : ∀ w ∈ K, ⟪c • x - c • orthogonal_projection_fn K x, w⟫ = 0,
+      { intros w hw,
+        rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero _ w hw, mul_zero] },
+      ext,
+      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
+    end }
+  1
+  (λ x, begin
+    simp only [one_mul, linear_map.coe_mk],
+    refine le_of_pow_le_pow 2 (norm_nonneg _) (by norm_num) _,
+    change ∥orthogonal_projection_fn K x∥ ^ 2 ≤ ∥x∥ ^ 2,
+    nlinarith [orthogonal_projection_fn_norm_sq K x]
+  end)
 
 @[simp]
 lemma orthogonal_projection_fn_eq {K : submodule 𝕜 E} [complete_space K] (v : E) :
-  orthogonal_projection_fn K v = orthogonal_projection K v :=
+  orthogonal_projection_fn K v = (orthogonal_projection K v : E) :=
 rfl
 
 /-- The characterization of the orthogonal projection.  -/
@@ -1629,6 +1648,11 @@ begin
   exact h
 end
 
+/-- The orthogonal projection has norm `≤ 1`. -/
+lemma orthogonal_projection_norm_le (K : submodule 𝕜 E) [complete_space K] :
+  ∥orthogonal_projection K∥ ≤ 1 :=
+linear_map.mk_continuous_norm_le _ (by norm_num) _
+
 /-- The subspace of vectors orthogonal to a given subspace. -/
 def submodule.orthogonal (K : submodule 𝕜 E) : submodule 𝕜 E :=
 { carrier := {v | ∀ u ∈ K, ⟪u, v⟫ = 0},

diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
@@ -835,9 +835,9 @@ def reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direct
           _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,
+        : 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, orthogonal_projection_linear]
+          ←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₂⟫