Unbounded

📁 Source: PhysLean/QuantumMechanics/OneDimension/Operators/Unbounded.lean

Statistics

Metric	Count
Definitions UnboundedOperator, IsGeneralizedEigenvector, IsSelfAdjoint, instCoeFunForallSubtypeAEEqFunRealComplexVolumeMemAddSubgroupHilbertSpace, ofSelfCLM	5
Theorems isGeneralizedEigenvector_ofSelfCLM_iff, ofSelfCLM_apply	2
Total	7

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
UnboundedOperator 📖	CompOp	—

QuantumMechanics.OneDimension.UnboundedOperator

Definitions

Name	Category	Theorems
IsGeneralizedEigenvector 📖	MathDef	3 math math: QuantumMechanics.OneDimension.positionStates_generalized_eigenvector_positionOperatorUnbounded, isGeneralizedEigenvector_ofSelfCLM_iff, QuantumMechanics.OneDimension.planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded
IsSelfAdjoint 📖	MathDef	3 math math: QuantumMechanics.OneDimension.HilbertSpace.parityOperatorUnbounded_isSelfAdjoint, QuantumMechanics.OneDimension.momentumOperatorUnbounded_isSelfAdjoint, QuantumMechanics.OneDimension.positionOperatorUnbounded_isSelfAdjoint
instCoeFunForallSubtypeAEEqFunRealComplexVolumeMemAddSubgroupHilbertSpace 📖	CompOp	—
ofSelfCLM 📖	CompOp	2 math math: isGeneralizedEigenvector_ofSelfCLM_iff, ofSelfCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneralizedEigenvector_ofSelfCLM_iff 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace	IsGeneralizedEigenvector ofSelfCLM	—	—
ofSelfCLM_apply 📖	mathematical	QuantumMechanics.OneDimension.HilbertSpace	ofSelfCLM	—	—

---

← Back to Index