diff --git a/PhysLean.lean b/PhysLean.lean index 22113a7f..cc3c7daa 100644 --- a/PhysLean.lean +++ b/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 diff --git a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean index 6a613a1c..67cdfb46 100644 --- a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean +++ b/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 diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index 3d8acce1..cc231eaa 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/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 diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index a93a5dc2..f7e0b231 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/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 diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Parity.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Parity.lean new file mode 100644 index 00000000..93caae5f --- /dev/null +++ b/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 diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index dcc056d7..278c7482 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/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