Completeness of the eigenfunctions of the Harmonic Oscillator

Completeness of the eigenfunctions follows from Plancherel's theorem.

The steps of this proof are:

1. Prove that if f is orthogonal to all eigenvectors then the Fourier transform of it muliplied by exp(-c x^2) for a 0<c is zero. Part of this is using the concept of dominated_convergence.
2. Use 'Plancherel's theorem' to show that f is zero.

theorem QuantumMechanics.OneDimension.HarmonicOscillator.mul_eigenfunction_integrable (Q : HarmonicOscillator) {n : ℕ} (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) : MeasureTheory.Integrable (fun (x : ℝ) => Q.eigenfunction n x * f x) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HarmonicOscillator.mul_physHermite_integrable (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HarmonicOscillator.mul_polynomial_integrable (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (P : Polynomial ℤ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑((fun (x : ℝ) => (Polynomial.aeval x) P) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) MeasureTheory.volume

theorem QuantumMechanics.OneDimension.HarmonicOscillator.mul_power_integrable (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (r : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) MeasureTheory.volume

Orthogonality conditions

theorem QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_eigenfunction_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (n : ℕ) : ∫ (x : ℝ), Q.eigenfunction n x * f x = 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_physHermite_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (n : ℕ) : ∫ (x : ℝ), ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_polynomial_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (P : Polynomial ℤ) : ∫ (x : ℝ), ↑((fun (x : ℝ) => (Polynomial.aeval x) P) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_power_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (r : ℕ) : ∫ (x : ℝ), ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = 0

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then it is orthogonal to

x ^ r * e ^ (- x ^ 2 / (2 ξ^2))

the proof of this result relies on the fact that Hermite polynomials span polynomials.

theorem QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_exp_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (c : ℝ) : ∫ (x : ℝ), Complex.exp (Complex.I * ↑c * ↑x) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = 0

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then it is orthogonal to

e ^ (I c x) * e ^ (- x ^ 2 / (2 ξ^2))

for any real c. The proof of this result relies on the expansion of e ^ (I c x) in terms of x^r/r! and using orthogonal_power_of_mem_orthogonal along with integrablity conditions.

theorem QuantumMechanics.OneDimension.HarmonicOscillator.fourierIntegral_zero_of_mem_orthogonal (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) : (Real.fourierIntegral fun (x : ℝ) => f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = 0

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then the fourier transform of

f (x) * e ^ (- x ^ 2 / (2 ξ^2))

is zero.

The proof of this result relies on orthogonal_exp_of_mem_orthogonal.

theorem QuantumMechanics.OneDimension.HarmonicOscillator.zero_of_orthogonal_mk (Q : HarmonicOscillator) (f : ℝ → ℂ) (hf : HilbertSpace.MemHS f) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) (HilbertSpace.mk hf) = 0) (plancherel_theorem : ∀ {f : ℝ → ℂ}, MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.eLpNorm (Real.fourierIntegral f) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume) : HilbertSpace.mk hf = 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.zero_of_orthogonal_eigenVector (Q : HarmonicOscillator) (f : ↥HilbertSpace) (hOrth : ∀ (n : ℕ), inner (HilbertSpace.mk ⋯) f = 0) (plancherel_theorem : ∀ {f : ℝ → ℂ}, MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.eLpNorm (Real.fourierIntegral f) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume) : f = 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness (Q : HarmonicOscillator) (plancherel_theorem : ∀ {f : ℝ → ℂ}, MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → MeasureTheory.eLpNorm (Real.fourierIntegral f) 2 MeasureTheory.volume = MeasureTheory.eLpNorm f 2 MeasureTheory.volume) : (Submodule.span ℂ (Set.range fun (n : ℕ) => HilbertSpace.mk ⋯)).topologicalClosure = ⊤

Assuming Plancherel's theorem (which is not yet in Mathlib), the topological closure of the span of the eigenfunctions of the harmonic oscillator is the whole Hilbert space.

The proof of this result relies on fourierIntegral_zero_of_mem_orthogonal and Plancherel's theorem which together give us that the norm of

f x * e ^ (- x^2 / (2 * ξ^2))

is zero for f orthogonal to all eigenfunctions, and hence the norm of f is zero.