Subspaces associated with orthogonal projections #
Here, the orthogonal projection is used to prove a series of more subtle lemmas about the
orthogonal complement of subspaces of E (the orthogonal complement itself was
defined in Analysis.InnerProductSpace.Orthogonal) such that they admit
orthogonal projections; the lemma
Submodule.sup_orthogonal_of_hasOrthogonalProjection,
stating that for a subspace K of E such that K admits an orthogonal projection we have
K â KᎠ= â¤, is a typical example.
If Kâ admits an orthogonal projection and is contained in Kâ,
then Kâ and KâᎠâ Kâ span Kâ.
Alias of Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection.
If Kâ admits an orthogonal projection and is contained in Kâ,
then Kâ and KâᎠâ Kâ span Kâ.
If K admits an orthogonal projection, then K and KᎠspan the whole space.
Alias of Submodule.sup_orthogonal_of_hasOrthogonalProjection.
If K admits an orthogonal projection, then K and KᎠspan the whole space.
If K admits an orthogonal projection, then the orthogonal complement of its orthogonal
complement is itself.
In a Hilbert space, the orthogonal complement of the orthogonal complement of a subspace K
is the topological closure of K.
Note that the completeness assumption is necessary. Let E be the space â ââ â with inner space
structure inherited from PiLp 2 (fun _ : â ⌠â). Let K be the subspace of sequences with the sum
of all elements equal to zero. Then KᎠ= âĽ, KáŽáŽ = â¤.
If K admits an orthogonal projection, K and KᎠare complements of each other.
Alias of Submodule.isCompl_orthogonal_of_hasOrthogonalProjection.
If K admits an orthogonal projection, K and KᎠare complements of each other.
Given a monotone family U of complete submodules of E and a fixed x : E,
the orthogonal projection of x on U i tends to the orthogonal projection of x on
(⨠i, U i).topologicalClosure along atTop.
Alias of Submodule.starProjection_tendsto_closure_iSup.
Given a monotone family U of complete submodules of E and a fixed x : E,
the orthogonal projection of x on U i tends to the orthogonal projection of x on
(⨠i, U i).topologicalClosure along atTop.
Given a monotone family U of complete submodules of E with dense span supremum,
and a fixed x : E, the orthogonal projection of x on U i tends to x along at_top.
Alias of Submodule.starProjection_tendsto_self.
Given a monotone family U of complete submodules of E with dense span supremum,
and a fixed x : E, the orthogonal projection of x on U i tends to x along at_top.
The orthogonal complement satisfies KáŽáŽáŽ = KáŽ.
The closure of K is the full space iff KᎠis trivial.
Alias of Submodule.orthogonalProjection_eq_linearProjOfIsCompl.
Alias of Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl.
If S is dense and x - y â KáŽ, then x = y.