Reducing subspaces of inner-product spaces

A subspace reduces an endomorphism when both it and its orthogonal complement are invariant. For a symmetric endomorphism, invariance of the subspace alone is enough. When an orthogonal projection exists, reduction is equivalently commutation with that projection; in particular the orthogonal projection onto a subspace invariant under a symmetric endomorphism commutes with it. More generally, an idempotent whose range and kernel are orthogonal both for the inner product and for the form of a symmetric endomorphism commutes with that endomorphism (LinearMap.IsSymmetric.commute_of_isIdempotentElem).

For a bounded operator A on a Hilbert space and a complete subspace invariant under both A and its adjoint, the adjoint of the restriction of A is the restriction of the adjoint (ContinuousLinearMap.adjoint_restrict), so the restriction of a normal operator is normal (IsStarNormal.restrict).

def Submodule.IsReducing {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) (A : Module.End 𝕜 E) : Prop

A subspace is reducing for an endomorphism when both it and its orthogonal complement are invariant under the endomorphism.

theorem Submodule.isReducing_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) (A : Module.End 𝕜 E) : U.IsReducing A ↔ U ∈ A.invtSubmodule ∧ Uᗮ ∈ A.invtSubmodule

A subspace is reducing exactly when it and its orthogonal complement are invariant.

theorem Submodule.IsReducing.mem_invtSubmodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {A : Module.End 𝕜 E} (hU : U.IsReducing A) : U ∈ A.invtSubmodule

A reducing subspace is invariant under the endomorphism.

theorem Submodule.IsReducing.orthogonal_mem_invtSubmodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} {A : Module.End 𝕜 E} (hU : U.IsReducing A) : Uᗮ ∈ A.invtSubmodule

The orthogonal complement of a reducing subspace is invariant under the endomorphism.

@[simp]

theorem Submodule.isReducing_orthogonal_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : Module.End 𝕜 E) : Uᗮ.IsReducing A ↔ U.IsReducing A

The orthogonal complement reduces an endomorphism exactly when the original subspace does.

theorem LinearMap.IsSymmetric.isReducing_iff_mem_invtSubmodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} (hA : IsSymmetric A) (U : Submodule 𝕜 E) : U.IsReducing A ↔ U ∈ A.invtSubmodule

A subspace reduces a symmetric endomorphism exactly when it is invariant.

theorem Submodule.isReducing_iff_commute_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (A : Module.End 𝕜 E) : U.IsReducing A ↔ Commute (↑U.starProjection) A

A subspace admitting an orthogonal projection reduces an endomorphism exactly when its orthogonal projection commutes with that endomorphism.

theorem LinearMap.IsSymmetric.starProjection_apply_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} (hA : IsSymmetric A) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : U ∈ A.invtSubmodule) (x : E) : U.starProjection (A x) = A (U.starProjection x)

The orthogonal projection onto a subspace invariant under a symmetric endomorphism commutes with that endomorphism.

theorem LinearMap.IsSymmetric.commute_of_isIdempotentElem {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A p : Module.End 𝕜 E} (hA : IsSymmetric A) (hp : IsIdempotentElem p) (hpp : ∀ (x y : E), inner 𝕜 (p x) (y - p y) = 0) (hAp : ∀ (x y : E), inner 𝕜 (A (p x)) (y - p y) = 0) : Commute p A

An idempotent endomorphism p whose range is orthogonal to its kernel, both for the inner product and for the form ⟪A ·, ·⟫ of a symmetric endomorphism A, commutes with A: its range and its kernel are invariant under A.

@[simp]

theorem Submodule.isReducing_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} : ⊥.IsReducing A

The zero subspace reduces every endomorphism.

@[simp]

theorem Submodule.isReducing_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} : ⊤.IsReducing A

The whole space reduces every endomorphism.

theorem Submodule.IsReducing.iSup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} {ι : Type u_3} {U : ι → Submodule 𝕜 E} (hU : ∀ (i : ι), (U i).IsReducing A) : (⨆ (i : ι), U i).IsReducing A

The supremum of a family of reducing subspaces is reducing.

theorem Submodule.IsReducing.sup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} {A : Module.End 𝕜 E} (hU : U.IsReducing A) (hV : V.IsReducing A) : (U ⊔ V).IsReducing A

The span of two reducing subspaces is reducing.

theorem Submodule.isReducing_coe_iff_commute_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : U.IsReducing ↑A ↔ Commute U.starProjection A

A subspace with an orthogonal projection reduces a bounded operator A exactly when A commutes with the orthogonal projection onto it.

theorem ContinuousLinearMap.isReducing_iff_mem_invtSubmodule_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [CompleteSpace E] [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : U.IsReducing ↑A ↔ U ∈ Module.End.invtSubmodule ↑A ∧ U ∈ Module.End.invtSubmodule ↑(adjoint A)

A subspace with an orthogonal projection reduces a bounded operator A on a Hilbert space exactly when it is invariant under both A and its adjoint.

@[simp]

theorem ContinuousLinearMap.isReducing_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [CompleteSpace E] [U.HasOrthogonalProjection] {A : E →L[𝕜] E} : U.IsReducing ↑(adjoint A) ↔ U.IsReducing ↑A

A subspace with an orthogonal projection reduces the adjoint of a bounded operator A on a Hilbert space exactly when it reduces A.

theorem Module.End.isReducing_iff_mem_invtSubmodule_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 E] {A : End 𝕜 E} : U.IsReducing A ↔ U ∈ A.invtSubmodule ∧ U ∈ invtSubmodule (LinearMap.adjoint A)

On a finite-dimensional space, a subspace reduces an endomorphism A exactly when it is invariant under both A and its adjoint.

@[simp]

theorem Module.End.isReducing_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 E] {A : End 𝕜 E} : U.IsReducing (LinearMap.adjoint A) ↔ U.IsReducing A

On a finite-dimensional space, a subspace reduces the adjoint of an endomorphism A exactly when it reduces A.

theorem LinearMap.IsSymmetric.sylvester_starProjection_orthogonal_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : U ∈ Module.End.invtSubmodule A) (X : F →ₗ[𝕜] E) (M : F →ₗ[𝕜] F) : A ∘ₗ ↑Uᗮ.starProjection ∘ₗ X - (↑Uᗮ.starProjection ∘ₗ X) ∘ₗ M = ↑Uᗮ.starProjection ∘ₗ (A ∘ₗ X - X ∘ₗ M)

For an invariant subspace of a symmetric map, applying the complementary projection to A X - X M is the same as forming the residual of the projected trial map. No isometry or finite-dimensionality hypothesis is needed.

The corresponding DKPS projected-residual statement is in ForTauCeti/Analysis/InnerProductSpace/Residual/AngleEmbedding.lean (Jon Crall and GPT 5.6 High; Kitware, Apache-2.0). The proof uses invariant-projection commutation.

theorem ContinuousLinearMap.adjoint_restrict {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {U : Submodule 𝕜 E} [CompleteSpace ↥U] {A : E →L[𝕜] E} (hA : ∀ x ∈ U, A x ∈ U) (hA' : ∀ x ∈ U, (adjoint A) x ∈ U) : adjoint (A.restrict hA) = (adjoint A).restrict hA'

The adjoint of the restriction of a bounded operator A to a complete subspace invariant under both A and its adjoint is the restriction of the adjoint.

theorem IsStarNormal.restrict {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {U : Submodule 𝕜 E} [CompleteSpace ↥U] {A : E →L[𝕜] E} (hN : IsStarNormal A) (hA : ∀ x ∈ U, A x ∈ U) (hA' : ∀ x ∈ U, (ContinuousLinearMap.adjoint A) x ∈ U) : IsStarNormal (A.restrict hA)

The restriction of a normal operator to a complete subspace invariant under both the operator and its adjoint is normal.