Theorems · Theorem · operator theory

LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces

∀ {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E},
  (∀ (i : n), LinearMap.IsSymmetric (T i)) →
    OrthogonalFamily 𝕜 (fun γ => ↥(⨅ j, (T j).eigenspace (γ j))) fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ

The joint eigenspaces of a family of symmetric operators form an OrthogonalFamily.

Defined in: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Cited by: 1 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike NormedAddCommGroup InnerProductSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
NormedAddCommGroupstatement and proof · cited by 15,752
Submodulestatement · cited by 7,192
InnerProductSpacestatement and proof · cited by 3,523
RCLikestatement and proof · cited by 2,829
iInfstatement and proof · cited by 1,690
Inner.innerproof · cited by 1,089
Module.Endstatement and proof · cited by 774
LinearMap.IsSymmetricstatement and proof · cited by 121
Module.End.eigenspacestatement and proof · cited by 56
OrthogonalFamilystatement · cited by 48
Submodule.subtypeₗᵢstatement and proof · cited by 42

Cited by1

Results whose statement or proof uses this declaration.

LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commuteproof · cited by 1