Parity

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

Statistics

Metric	Count
Definitions parityOperator, parityOperatorSchwartz, parityOperatorUnbounded	3
Theorems parityOperatorSchwartz_parityOperatorSchwartz, parityOperatorUnbounded_isSelfAdjoint	2
Total	5

QuantumMechanics.OneDimension.HilbertSpace

Definitions

Name	Category	Theorems
parityOperator 📖	CompOp	2 math math: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity, QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity
parityOperatorSchwartz 📖	CompOp	1 math math: parityOperatorSchwartz_parityOperatorSchwartz
parityOperatorUnbounded 📖	CompOp	1 math math: parityOperatorUnbounded_isSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
parityOperatorSchwartz_parityOperatorSchwartz 📖	mathematical	—	parityOperatorSchwartz	—	—
parityOperatorUnbounded_isSelfAdjoint 📖	mathematical	—	QuantumMechanics.OneDimension.UnboundedOperator.IsSelfAdjoint schwartzIncl schwartzIncl_injective parityOperatorUnbounded	—	schwartzIncl_inner

---

← Back to Index