English
Let E be a real or complex inner product space and K a subspace that has an orthogonal complement K⊥ such that E = K ⊕ K⊥. Then for every x ∈ E, the orthogonal projection of x onto K coincides with the projection determined by the direct sum decomposition E = K ⊕ K⊥.
Русский
Пусть E — вещественное или комплексное эрмп-пространство и K — подпространство, имеющее ортогональное дополнение K⊥ так, что E = K ⊕ K⊥. Тогда для каждого x ∈ E ортотпроекция x на K совпадает с проекцией, получаемой из разложения E на прямую сумму K ⊕ K⊥.
LaTeX
$$$\\forall x\\in E:\\; P_K(x) = \\mathrm{Proj}_{K}^{K^\\perp}(x),$ где $E = K \\oplus K^\\perp$.$$
Lean4
theorem orthogonalProjection_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] (x : E) :
K.orthogonalProjection x = K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection x :=
by
have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
conv_lhs => rw [← IsCompl.projection_add_projection_eq_self this x]
simp_rw [IsCompl.projection_apply]
rw [map_add, orthogonalProjection_mem_subspace_eq_self,
orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
