English
In a complete space E with a subspace K having an orthogonal projection, the identity map equals the sum of the projections onto K and onto its orthogonal complement.
Русский
В полнораспределенном пространстве E с подпространством K, имеющим ортогональную проекцию, тождество равно сумме проекций onto K и onto K⊥.
LaTeX
$$$ \mathrm{id}_E = P_K + P_{K^{\perp}}. $$$
Lean4
/-- The Pythagorean theorem, for an orthogonal projection. -/
theorem norm_sq_eq_add_norm_sq_projection (x : E) (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] :
‖x‖ ^ 2 = ‖S.orthogonalProjection x‖ ^ 2 + ‖Sᗮ.orthogonalProjection x‖ ^ 2 :=
calc
‖x‖ ^ 2 = ‖S.starProjection x + Sᗮ.starProjection x‖ ^ 2 := by rw [starProjection_add_starProjection_orthogonal]
_ = ‖S.orthogonalProjection x‖ ^ 2 + ‖Sᗮ.orthogonalProjection x‖ ^ 2 :=
by
simp only [sq]
exact
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
(S.mem_orthogonal _).1 (Sᗮ.orthogonalProjection x).2 _ (S.orthogonalProjection x).2
