DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Parity operator

Browse source
This commit is contained in:
jstoobysmith 2025-02-27 06:34:14 +00:00
parent c0c0f28049
commit 4c9e2053ee
6 changed files with 102 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/MetaPrograms/notes.lean
View file

@ -314,9 +314,12 @@ def harmonicOscillator : Note where
.name ``QuantumMechanics.OneDimension.HilbertSpace.MemHS .complete,
.name ``QuantumMechanics.OneDimension.HilbertSpace.memHS_iff .complete,
.name ``QuantumMechanics.OneDimension.HilbertSpace.mk .complete,
.name ``QuantumMechanics.OneDimension.HilbertSpace.parity .complete,
.name ``QuantumMechanics.OneDimension.HilbertSpace.memHS_of_parity .complete,
.h1 "The Schrodinger Operator",
.name ``QuantumMechanics.OneDimension.HarmonicOscillator .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity .complete,
.h1 "The eigenfunctions of the Schrodinger Operator",
.name ``PhysLean.physHermite .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction .complete,
@ -328,6 +331,7 @@ def harmonicOscillator : Note where
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity .complete,
.h1 "The time-independent Schrodinger Equation",
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue .complete,
.name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction