Physicslib4.Operators.ReducingSubspace
Reducing subspaces #
A closed subspace K of a complex Hilbert space that is invariant under an operator T and
under its adjoint reduces T: the orthogonal projection onto K commutes with T.
Blueprint reference: lmm:reducing-subspace-projection-commutes.
theorem
Physicslib4.commute_starProjection_of_invariant
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
[CompleteSpace E]
(K : Submodule ℂ E)
[K.HasOrthogonalProjection]
(T : E →L[ℂ] E)
(hT : ∀ x ∈ K, T x ∈ K)
(hT' : ∀ x ∈ K, (ContinuousLinearMap.adjoint T) x ∈ K)
:
A reducing subspace commutes with the operator. If T and its adjoint both map the
subspace K into itself, then the orthogonal projection onto K commutes with T.
Blueprint reference: lmm:reducing-subspace-projection-commutes.