1. Physlib
  2. QuantumMechanics
  3. HarmonicOscillator
  4. OneDimension
  5. Completeness
Imports
/- 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 -/ module public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Gaussians

Completeness of the eigenfunctions of the Harmonic Oscillator

Completeness of the eigenfunctions follows from Plancherel's theorem.

The steps of this proof are:

    Prove that if f is orthogonal to all eigenvectors then the Fourier transform of it multiplied by exp(-c x^2) for a 0<c is zero. Part of this is using the concept of dominated_convergence.

    Use 'Plancherel's theorem' to show that f is zero.

@[expose] public section/- Integrability conditions related to eigenfunctions. -/ lemma mul_eigenfunction_integrable (f : ℝ → ℂ) (hf : MemHS f) : MeasureTheory.Integrable (fun x => Q.eigenfunction n x * f x) := Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS f⊢ Integrable (fun x => Q.eigenfunction n x * f x) volume Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ Integrable (fun x => Q.eigenfunction n x * f x) volume Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) =ᵐ[volume] fun x => Q.eigenfunction n x * f x Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => ↑↑(HilbertSpace.mk hf) x * (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x)) =ᵐ[volume] fun x => Q.eigenfunction n x * f x conv_lhs => Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volumex:ℝ| ↑↑(HilbertSpace.mk hf) x * (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x); Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volumex:ℝ| (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x) * ↑↑(HilbertSpace.mk hf) x Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x)) =ᵐ[volume] Q.eigenfunction nQ:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ ↑↑(HilbertSpace.mk hf) =ᵐ[volume] f Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ ↑↑(HilbertSpace.mk hf) =ᵐ[volume] fQ:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x)) =ᵐ[volume] Q.eigenfunction n Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ ↑↑(HilbertSpace.mk hf) =ᵐ[volume] f All goals completed! 🐙 Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x)) =ᵐ[volume] fun x => (starRingEnd ℂ) (Q.eigenfunction n x)Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (Q.eigenfunction n x)) =ᵐ[volume] Q.eigenfunction n Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (↑↑(HilbertSpace.mk ⋯) x)) =ᵐ[volume] fun x => (starRingEnd ℂ) (Q.eigenfunction n x) Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ ↑↑(HilbertSpace.mk ⋯) =ᵐ[volume] Q.eigenfunction n All goals completed! 🐙 Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (Q.eigenfunction n x)) =ᵐ[volume] Q.eigenfunction n Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volume⊢ (fun x => (starRingEnd ℂ) (Q.eigenfunction n x)) = Q.eigenfunction n Q:HarmonicOscillatorn:ℕf:ℝ → ℂhf:MemHS fh1:Integrable (fun x => ⟪↑↑(HilbertSpace.mk ⋯) x, ↑↑(HilbertSpace.mk hf) x⟫_ℂ) volumex:ℝ⊢ (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x All goals completed! 🐙Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable (fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ Integrable (fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volumeQ:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ IsUnit (1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable (fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ Integrable (fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume All goals completed! 🐙 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬n ! = 0 ∧ ¬√Q.ξ = 0 ∧ ¬√Real.pi = 0 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬n ! = 0Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Q.ξ = 0 ∧ ¬√Real.pi = 0 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬n ! = 0 All goals completed! 🐙 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Q.ξ = 0 ∧ ¬√Real.pi = 0 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Q.ξ = 0Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Real.pi = 0 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Q.ξ = 0 All goals completed! 🐙 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fn:ℕh2:((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh1:Integrable ((1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ))) • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume⊢ ¬√Real.pi = 0 All goals completed! 🐙Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fP:Polynomial ℤa:ℕ →₀ ℝha:(a.sum fun i a => a • fun x => (Polynomial.aeval x) (physHermite i)) = fun x => (Polynomial.aeval x) Ph2:(fun x => ↑((fun x => (Polynomial.aeval x) P) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => ∑ r ∈ a.support, ↑(a r) * ↑((fun x => (Polynomial.aeval x) (physHermite r)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))i:ℕhi:i ∈ a.supporthf':(fun x => ↑(a i) * (↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))) = fun x => a i • (↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))⊢ Integrable (fun x => a i • (↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))) volume Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fP:Polynomial ℤa:ℕ →₀ ℝha:(a.sum fun i a => a • fun x => (Polynomial.aeval x) (physHermite i)) = fun x => (Polynomial.aeval x) Ph2:(fun x => ↑((fun x => (Polynomial.aeval x) P) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => ∑ r ∈ a.support, ↑(a r) * ↑((fun x => (Polynomial.aeval x) (physHermite r)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))i:ℕhi:i ∈ a.supporthf':(fun x => ↑(a i) * (↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))) = fun x => a i • (↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))))⊢ Integrable (fun i_1 => ↑((fun x => (Polynomial.aeval x) (physHermite i)) (i_1 / Q.ξ)) * (f i_1 * ↑(Real.exp (-i_1 ^ 2 / (2 * Q.ξ ^ 2))))) volume All goals completed! 🐙Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fr:ℕhr:r ≠ 0h1:Integrable ((1 / ↑Q.ξ) ^ r • fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volumeh2:(fun x => (↑x / ↑Q.ξ) ^ r * (f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) = (1 / ↑Q.ξ) ^ r • fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))⊢ IsUnit ((1 / ↑Q.ξ) ^ r) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fr:ℕhr:r ≠ 0h1:Integrable ((1 / ↑Q.ξ) ^ r • fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volumeh2:(fun x => (↑x / ↑Q.ξ) ^ r * (f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) = (1 / ↑Q.ξ) ^ r • fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))⊢ 1 / ↑Q.ξ = 0 → r = 0 All goals completed! 🐙 Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fr:ℕhr:¬r ≠ 0⊢ Integrable (fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fr:ℕhr:r = 0⊢ Integrable (fun x => ↑x ^ r * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS f⊢ Integrable (fun x => ↑x ^ 0 * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume All goals completed! 🐙

Orthogonality conditions

Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0n:ℕ⊢ ∫ (x : ℝ), Q.eigenfunction n x * f x = ∫ (x : ℝ), (starRingEnd ℂ) (Q.eigenfunction n x) * f x All goals completed! 🐙local notation "m" => Q.mlocal notation "ℏ" => Q.ℏlocal notation "ω" => Q.ωlocal notation "hm" => Q.hmlocal notation "hℏ" => Q.hℏlocal notation "hω" => Q.hωQ:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0n:ℕh2:(fun x => 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * (↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh0:n ! ≠ 0h0':¬(√Q.ξ = 0 ∨ √Real.pi = 0)h1:∫ (a : ℝ), ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) = 0⊢ ∫ (x : ℝ), ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = ∫ (a : ℝ), ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0n:ℕh2:(fun x => 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * (↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh0:n ! ≠ 0h0':¬(√Q.ξ = 0 ∨ √Real.pi = 0)h1:∫ (a : ℝ), ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) = 0⊢ (fun x => ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun a => ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0n:ℕh2:(fun x => 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * (↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh0:n ! ≠ 0h0':¬(√Q.ξ = 0 ∨ √Real.pi = 0)h1:∫ (a : ℝ), ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) = 0x:ℝ⊢ ↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = ↑((Polynomial.aeval (x / Q.ξ)) (physHermite n)) * f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0n:ℕh2:(fun x => 1 / ↑√(2 ^ n * ↑n !) * (1 / ↑√(√Real.pi * Q.ξ)) * (↑((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ)) * f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => Q.eigenfunction n x * f xh0:n ! ≠ 0h0':¬(√Q.ξ = 0 ∨ √Real.pi = 0)h1:∫ (a : ℝ), ↑((Polynomial.aeval (a / Q.ξ)) (physHermite n)) * f a * Complex.exp (-↑a ^ 2 / (2 * ↑Q.ξ ^ 2)) = 0x:ℝ⊢ ↑((Polynomial.aeval (x / Q.ξ)) (physHermite n)) * (f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) = ↑((Polynomial.aeval (x / Q.ξ)) (physHermite n)) * f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) All goals completed! 🐙Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0P:Polynomial ℤa:ℕ →₀ ℝha:(a.sum fun i a => a • fun x => (Polynomial.aeval x) (physHermite i)) = fun x => (Polynomial.aeval x) Ph2:(fun x => ↑((fun x => (Polynomial.aeval x) P) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = fun x => ∑ r ∈ a.support, ↑(a r) * ↑((fun x => (Polynomial.aeval x) (physHermite r)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))i:ℕhi:i ∈ a.supporthf':(fun x => ↑(a i) * ↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) = a i • fun x => ↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))⊢ Integrable (fun x => ↑(a i) * ↑((fun x => (Polynomial.aeval x) (physHermite i)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2))))) volume All goals completed! 🐙

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.

Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0⊢ ∫ (x : ℝ), f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) = ∫ (x : ℝ), ↑((fun x => (Polynomial.aeval x) (physHermite 0)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0⊢ (fun x => f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) = fun x => ↑((fun x => (Polynomial.aeval x) (physHermite 0)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫_ℂ = 0x:ℝ⊢ f x * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) = ↑((fun x => (Polynomial.aeval x) (physHermite 0)) (x / Q.ξ)) * (f x * ↑(Real.exp (-x ^ 2 / (2 * Q.ξ ^ 2)))) All goals completed! 🐙

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 integrability conditions.

All goals completed! 🐙

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.

Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝ⊢ ∫ (v : ℝ), 𝐞 (-(c * v)) • (f v * cexp (-↑v ^ 2 / (2 * ↑Q.ξ ^ 2))) = ∫ (x : ℝ), cexp (I * ↑(-2 * π * c) * ↑x) * (f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝ⊢ (fun v => 𝐞 (-(c * v)) • (f v * cexp (-↑v ^ 2 / (2 * ↑Q.ξ ^ 2)))) = fun x => cexp (I * ↑(-2 * π * c) * ↑x) * (f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝx:ℝ⊢ 𝐞 (-(c * x)) • (f x * cexp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) = cexp (I * ↑(-2 * π * c) * ↑x) * (f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝx:ℝ⊢ ⟨cexp (-(2 * ↑π * (↑c * ↑x) * I)), ⋯⟩ • (f x * cexp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) = cexp (-(I * (2 * ↑π * ↑c) * ↑x)) * (f x * cexp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝx:ℝ⊢ cexp (-(2 * ↑π * (↑c * ↑x) * I)) * (f x * cexp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) = cexp (-(I * (2 * ↑π * ↑c) * ↑x)) * (f x * cexp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0c:ℝx:ℝ⊢ -(2 * ↑π * (↑c * ↑x) * I) = -(I * (2 * ↑π * ↑c) * ↑x) All goals completed! 🐙
Q:HarmonicOscillatorf:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0plancherel_theorem:∀ {f : ℝ → ℂ}, Integrable f volume → MemLp f 2 volume → eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volumehf':(fun x => f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) = fun x => f x * ↑(rexp (-(1 / (2 * Q.ξ ^ 2)) * (x - 0) ^ 2))hInt:MemLp (fun x => f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) 1 volumeh1:eLpNorm (fun x => f x * ↑(rexp (-x ^ 2 / (2 * Q.ξ ^ 2)))) 2 volume = 0h2:eLpNorm f 2 volume = 0⊢ ENNReal.toReal 0 = 0 All goals completed! 🐙lemma zero_of_orthogonal_eigenVector (f : HilbertSpace) (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), f⟫_ℂ = 0) (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : MemLp f 2), eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : f = 0 := Q:HarmonicOscillatorf:↥HilbertSpacehOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, f⟫ = 0plancherel_theorem:∀ {f : ℝ → ℂ}, Integrable f volume → MemLp f 2 volume → eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume⊢ f = 0 Q:HarmonicOscillatorplancherel_theorem:∀ {f : ℝ → ℂ}, Integrable f volume → MemLp f 2 volume → eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volumef:ℝ → ℂhf:MemHS fhOrth:∀ (n : ℕ), ⟪HilbertSpace.mk ⋯, HilbertSpace.mk hf⟫ = 0⊢ HilbertSpace.mk hf = 0 All goals completed! 🐙

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.

Q:HarmonicOscillatorplancherel_theorem:∀ {f : ℝ → ℂ}, Integrable f volume → MemLp f 2 volume → eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volumef:↥HilbertSpacehf:∀ u ∈ Submodule.span ℂ (Set.range fun n => HilbertSpace.mk ⋯), ⟪f, u⟫ = 0n:ℕhl:⟪f, HilbertSpace.mk ⋯⟫ = 0⊢ (starRingEnd ℂ) 0 = 0 All goals completed! 🐙