Map · 47
operator theory
MSC 47 · Operator theory
359 declarations (312 theorems, 47 definitions) across 13 files. 0 of the 12 famous theorems listed for this area are in Mathlib (0%). 19 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas2
- 47B Special classes of linear operators 221
- 47A General theory of linear operators 138
Famous theorems0 of 12
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 12
Open conjectures stated in Lean19
Statements without proofs, collected by the Formal Conjectures project.
- OpenQuantumProblem23.hasSICPOVM_56OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_58OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_59OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_60OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_64OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_68OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_69OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_70OpenQuantumProblems
- OpenQuantumProblem23.hasSICPOVM_71OpenQuantumProblems
Files13
Largest first. The code after each file is its assigned subarea.
- Mathlib.Analysis.InnerProductSpace.Positive
Positive operators
47B · 87
- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
Fredholm operators between topological vector spaces
47A · 53
- Mathlib.Analysis.InnerProductSpace.Symmetric
Symmetric linear maps in an inner product space
47B · 50
- Mathlib.Analysis.Normed.Operator.Compact.Basic
Compact operators
47B · 46
- Mathlib.Analysis.InnerProductSpace.Spectrum
Spectral theory of self-adjoint operators
47A · 41
- Mathlib.Analysis.InnerProductSpace.LinearPMap
Partially defined linear operators on Hilbert spaces
47B · 31
- Mathlib.Analysis.InnerProductSpace.Rayleigh
The Rayleigh quotient
47A · 26
- Mathlib.Analysis.InnerProductSpace.JointEigenspace
Joint eigenspaces of commuting symmetric operators
47A · 8
- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
Strict linear maps with closed range are closed under finite-rank perturbation
47A · 5
- Mathlib.Analysis.InnerProductSpace.Trace
Traces in inner product spaces
47B · 4
- Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
Compact operators and finite dimensional spaces
47B · 3
- Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
Spectral theory of compact operators
47A · 3