feat(analysis/inner_product_space/projection): norm_sq_eq_sum_norm_sq… (

#12096)

…_projection

The Pythagorean theorem for an orthogonal projection onto a submodule S.
I am sure that there are some style changes that could/should be made!

Co-authored-by: Daniel Packer



Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>

src/analysis/inner_product_space/projection.lean

@@ -822,6 +822,23 @@ begin
     simp [hy] }
 end
 
+/-- The Pythagorean theorem, for an orthogonal projection.-/
+lemma norm_sq_eq_add_norm_sq_projection
+  (x : E) (S : submodule 𝕜 E) [complete_space E] [complete_space S] :
+  ∥x∥^2 = ∥orthogonal_projection S x∥^2 + ∥orthogonal_projection Sᗮ x∥^2 :=
+begin
+  let p1 := orthogonal_projection S,
+  let p2 := orthogonal_projection Sᗮ,
+  have x_decomp : x = p1 x + p2 x :=
+    eq_sum_orthogonal_projection_self_orthogonal_complement S x,
+  have x_orth : ⟪ p1 x, p2 x ⟫ = 0 :=
+    submodule.inner_right_of_mem_orthogonal (set_like.coe_mem (p1 x)) (set_like.coe_mem (p2 x)),
+  nth_rewrite 0 [x_decomp],
+  simp only [sq, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero ((p1 x) : E) (p2 x) x_orth,
+             add_left_inj, mul_eq_mul_left_iff, norm_eq_zero, true_or, eq_self_iff_true,
+             submodule.coe_norm, submodule.coe_eq_zero]
+end
+
 /-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
 complement sum to the identity. -/
 lemma id_eq_sum_orthogonal_projection_self_orthogonal_complement