Commit 2026-03-19 02:11 36f4d76b

View on Github →

feat(Analysis/InnerProductSpace/Spectrum): eigenspaces of a compact selfadjoint operator exhaust the Hilbert space (#36520) This PR proves that the eigenspaces of a compact self-adjoint operator are finite dimensional and have trivial orthogonal complement.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

added theorem ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero

added theorem ContinuousLinearMap.finite_dimensional_eigenspace

added theorem ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot

Modified Mathlib/Analysis/Normed/Group/Submodule.lean

added theorem LinearMap.continuous_domRestrict

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.eigenspace_mem_invtSubmodule

added theorem Module.End.genEigenspace_mem_invtSubmodule

added theorem Module.End.restrict_eigenspace

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean