diff --git a/PhysLean.lean b/PhysLean.lean index c9395afd..458af1fb 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -180,7 +180,7 @@ import PhysLean.PerturbationTheory.WickContraction.TimeCond import PhysLean.PerturbationTheory.WickContraction.TimeContract import PhysLean.PerturbationTheory.WickContraction.Uncontracted import PhysLean.PerturbationTheory.WickContraction.UncontractedList -import PhysLean.QuantumMechanics.HarmonicOscillator +import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator 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 61ebe846..913e85af 100644 --- a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean +++ b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean @@ -1,13 +1,5 @@ import Mathlib.Analysis.Calculus.Deriv.Polynomial -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.SpecialFunctions.Exp -import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral -import Mathlib.RingTheory.Polynomial.Hermite.Gaussian /-! # Physicists Hermite Polynomial diff --git a/PhysLean/QuantumMechanics/HarmonicOscillator.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator.lean similarity index 98% rename from PhysLean/QuantumMechanics/HarmonicOscillator.lean rename to PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator.lean index 45ef8685..821d7d08 100644 --- a/PhysLean/QuantumMechanics/HarmonicOscillator.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator.lean @@ -3,12 +3,6 @@ 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 Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Mathlib.Analysis.SpecialFunctions.Integrals -import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral -import Mathlib.RingTheory.Polynomial.Hermite.Gaussian import PhysLean.Mathematics.SpecialFunctions.PhyscisistsHermite /-!