English
For a subspace K of a Hilbert space E, the family of subspaces {K, K⊥} forms a Hilbert sum giving the space E as the orthogonal direct sum of K and its orthogonal complement.
Русский
Для подпространства K гильбертова пространства E совокупность K и K⊥ образуют гильбертову сумму, дающую пространство E как ортогональное прямое суммирование.
LaTeX
$$$ IsHilbertSum 𝕜 E (\\text{span}_{𝕜}(K) \\text{ и } K^{\\perp}) (i \\mapsto (\\text{Subtype}_{K}) ) $$$
Lean4
theorem isHilbertSumOrthogonal (K : Submodule 𝕜 E) [hK : CompleteSpace K] :
IsHilbertSum 𝕜 (fun b => ↥(cond b K Kᗮ)) fun b => (cond b K Kᗮ).subtypeₗᵢ :=
by
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
intro b
cases b <;>
first
| exact instOrthogonalCompleteSpace K
| assumption
refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_
refine le_trans ?_ (Submodule.le_topologicalClosure _)
rw [iSup_bool_eq, cond, cond]
refine Codisjoint.top_le ?_
exact Submodule.isCompl_orthogonal_of_hasOrthogonalProjection.codisjoint
