Merge pull request #352 from HEPLean/JTS/QuantumMechanics

feat: Parity operator

PhysLean.lean

@@ -186,6 +186,7 @@ import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Parity
 import PhysLean.SpaceTime.Basic
 import PhysLean.SpaceTime.CliffordAlgebra
 import PhysLean.StandardModel.Basic

PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean

@@ -148,6 +148,10 @@ lemma physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0 := by
 instance : CoeFun (Polynomial ℤ) (fun _ ↦ ℝ → ℝ)where
   coe p := fun x => p.aeval x
 
+lemma physHermite_eq_aeval (n : ℕ) (x : ℝ) :
+    physHermite n x = (physHermite n).aeval x := by
+  rfl
+
 lemma physHermite_zero_apply (x : ℝ) : physHermite 0 x = 1 := by
   simp [aeval]
 
@@ -219,6 +223,19 @@ lemma deriv_physHermite' (x : ℝ)
   rw [fderiv_physHermite (hf := by fun_prop)]
   rfl
 
+lemma physHermite_parity: (n : ℕ) → (x : ℝ) →
+    physHermite n (-x) = (-1)^n * physHermite n x
+  | 0, x => by simp
+  | 1, x => by
+    simp [physHermite_one, aeval]
+  | n + 2, x => by
+    rw [physHermite_succ_fun']
+    have h1 := physHermite_parity (n + 1) x
+    have h2 := physHermite_parity n x
+    simp only [smul_neg, nsmul_eq_mul, cast_ofNat, h1, neg_mul, cast_add, cast_one,
+      add_tsub_cancel_right, h2, smul_eq_mul]
+    ring
+
 /-!
 
 ## Relationship to Gaussians

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import PhysLean.Mathematics.SpecialFunctions.PhyscisistsHermite
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
+import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Parity
 /-!
 
 # 1d Harmonic Oscillator
@@ -102,6 +103,23 @@ lemma ℏ_ne_zero : Q.ℏ ≠ 0 := by
 noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
   fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y
 
+open HilbertSpace
+
+/-- The Schrodinger operator commutes with the parity operator. -/
+lemma schrodingerOperator_parity (ψ : ℝ → ℂ) :
+    Q.schrodingerOperator (parity ψ) = parity (Q.schrodingerOperator ψ) := by
+  funext x
+  simp only [schrodingerOperator, parity, LinearMap.coe_mk, AddHom.coe_mk, one_div,
+    Complex.ofReal_neg, even_two, Even.neg_pow, add_left_inj, mul_eq_mul_left_iff, div_eq_zero_iff,
+    neg_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff,
+    Complex.ofReal_eq_zero, _root_.mul_eq_zero, false_or]
+  left
+  have h1 (ψ : ℝ → ℂ) : (fun x => (deriv fun x => ψ (-x)) x) = fun x => - deriv ψ (-x) := by
+    funext x
+    rw [← deriv_comp_neg]
+  change deriv (fun x=> (deriv fun x => ψ (-x)) x) x = _
+  simp [h1]
+
 end HarmonicOscillator
 end OneDimension
 end QuantumMechanics

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
+import Mathlib.Topology.Algebra.Polynomial
 /-!
 
 # Eigenfunction of the Harmonic Oscillator
@@ -173,6 +174,24 @@ lemma eigenfunction_differentiableAt (x : ℝ) (n : ℕ) :
   rw [eigenfunction_eq]
   fun_prop
 
+/-- The eigenfunctions are continuous. -/
+@[fun_prop]
+lemma eigenfunction_continuous (n : ℕ) : Continuous (Q.eigenfunction n) := by
+  rw [eigenfunction_eq]
+  fun_prop
+
+/-- The `n`th eigenfunction is an eigenfunction of the parity operator with
+  the eigenvalue `(-1) ^ n`. -/
+lemma eigenfunction_parity (n : ℕ) :
+    parity (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction n := by
+  funext x
+  rw [eigenfunction_eq]
+  simp only [parity, LinearMap.coe_mk, AddHom.coe_mk, mul_neg, Pi.mul_apply, Pi.pow_apply,
+    Pi.neg_apply, Pi.one_apply]
+  rw [← physHermite_eq_aeval, physHermite_parity]
+  simp only [Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_neg, Complex.ofReal_one]
+  ring_nf
+
 /-!
 
 ## Orthnormality

PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Parity.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+/-!
+
+# Parity operator
+
+-/
+
+namespace QuantumMechanics
+
+namespace OneDimension
+noncomputable section
+
+namespace HilbertSpace
+open MeasureTheory
+
+/-- The parity operator is defined as linear map from `ℝ → ℂ` to itself, such that
+  `ψ` is taken to `fun x => ψ (-x)`. -/
+def parity : (ℝ → ℂ) →ₗ[ℂ] (ℝ → ℂ) where
+  toFun ψ := fun x => ψ (-x)
+  map_add' ψ1 ψ2 := by
+    funext x
+    simp
+  map_smul' a ψ1 := by
+    funext x
+    simp
+
+/-- The parity operator acting on a member of the Hilbert space is in Hilbert space. -/
+lemma memHS_of_parity (ψ : ℝ → ℂ) (hψ : MemHS ψ) : MemHS (parity ψ) := by
+  simp only [parity, LinearMap.coe_mk, AddHom.coe_mk]
+  rw [memHS_iff] at hψ ⊢
+  apply And.intro
+  · rw [show (fun x => ψ (-x)) = ψ ∘ (λ x => -x) by funext x; simp]
+    exact MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving hψ.left <|
+      quasiMeasurePreserving_neg_of_right_invariant volume
+  · simpa using (integrable_comp_mul_left_iff
+      (fun x => ‖ψ (x)‖ ^ 2) (R := (-1 : ℝ)) (by simp)).mpr hψ.right
+
+end HilbertSpace

scripts/MetaPrograms/notes.lean

@@ -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