norm_sq_eq_add_norm_sq_starProjection

English

For a subspace S with an orthogonal projection, the Pythagorean identity holds: ||x||^2 = ||P_S x||^2 + ||P_{S^{\perp}} x||^2.

Русский

Для подпространства S с ортогональной проекцией выполняется тождество Пифагора: ||x||^2 = ||P_S x||^2 + ||P_{S^{\perp}} x||^2.

LaTeX

$$$ \|x\|^2 = \|S.orthogonalProjection(x)\|^2 + \|S^{\perp}.orthogonalProjection(x)\|^2. $$$

Lean4

theorem norm_sq_eq_add_norm_sq_starProjection (x : E) (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] :
    ‖x‖ ^ 2 = ‖S.starProjection x‖ ^ 2 + ‖Sᗮ.starProjection x‖ ^ 2 :=
  norm_sq_eq_add_norm_sq_projection x S

Похожие утверждения