The Quantum Harmonic Oscillator
Note Authors: Joseph Tooby-Smith
These notes are created using an interactive theorem
prover called Lean.
Lean formally checks definitions, theorems and proofs for correctness.
These notes are part of a much larger project called
PhysLean, which aims to digitalize
physics into Lean. Please consider contributing to this project.
Please provide feedback or suggestions for improvements by creating a GitHub issue
here.
Table of content
1. Introduction
2. Hilbert Space
3. The Schrodinger Operator
4. The eigenfunctions of the Schrodinger Operator
4.1. Properties of the eigenfunctions
5. The time-independent Schrodinger Equation
6. Completeness
1. Introduction
The quantum harmonic oscillator is a fundamental example of a one-dimensional quantum mechanical system. It is often one of the first models encountered by undergraduate students studying quantum mechanics.
This note presents the formalization of the quantum harmonic oscillator in the theorem prover Lean 4, as part of the larger project PhysLean. What this means is that every definition and theorem in this note has been formally checked for mathematical correctness for by a computer. There are a number of motivations for doing this which are dicussed here.
Note that we do not give every definition and theorem which is part of the formalization. Our goal is give key aspects, in such a way that we hope this note will be useful to newcomers to Lean or those intrested in simply intrested in learning about the quantum harmonic oscillator.
2. Hilbert Space
The Hilbert space for a one dimensional quantum system is defined as
the space of almost-everywhere equal equivalence classes of square integrable functions
from ℝ to ℂ.
Show Lean code:
noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
The proposition MemHS f for a function f : ℝ → ℂ is defined
to be true if the function f can be lifted to the Hilbert space.
Show Lean code:
def MemHS (f : ℝ → ℂ) : Prop := MemLp f 2 MeasureTheory.volume
A function f statisfies MemHS f if and only if it is almost everywhere
strongly measurable, and square integrable.
Show Lean code:
lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by
rw [MemHS]
simp [MemLp, and_congr_right_iff]
intro h1
rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
(Ne.symm (NeZero.ne' 2)) ENNReal.ofNat_ne_top]
simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat, Integrable]
have h0 : MeasureTheory.AEStronglyMeasurable
(fun x => norm (f x) ^ 2) MeasureTheory.volume := by
apply MeasureTheory.AEStronglyMeasurable.pow
exact Continuous.comp_aestronglyMeasurable continuous_norm h1
simp only [h0, true_and]
simp only [HasFiniteIntegral, enorm_pow]
simp only [enorm, nnnorm, Real.norm_eq_abs, abs_norm]
Given a function f : ℝ → ℂ such that MemHS f is true via hf, then HilbertSpace.mk hf
is the element of the HilbertSpace defined by f.
Show Lean code:
def mk {f : ℝ → ℂ} (hf : MemHS f) : HilbertSpace :=
⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩
The parity operator is defined as linear map from ℝ → ℂ to itself, such that
ψ is taken to fun x => ψ (-x).
Show Lean code:
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.
Show Lean code:
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
3. The Schrodinger Operator
A quantum harmonic oscillator specified by a three
real parameters: the mass of the particle m, a value of Planck’s constant ℏ, and
an angular frequency ω. All three of these parameters are assumed to be positive.
Show Lean code:
structure HarmonicOscillator where
/-- The mass of the particle. -/
m : ℝ
/-- Reduced Planck's constant. -/
ℏ : ℝ
/-- The angular frequency of the harmonic oscillator. -/
ω : ℝ
hℏ : 0 < ℏ
hω : 0 < ω
hm : 0 < m
The characteristic length ξ of the harmonic oscillator is defined
as √(ℏ /(m ω)).
Show Lean code:
noncomputable def ξ : ℝ := √(Q.ℏ / (Q.m * Q.ω))
For a harmonic oscillator, the Schrodinger Operator corresponding to it
is defined as the function from ℝ → ℂ to ℝ → ℂ taking
ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ.
Show Lean code:
noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
fun x => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) x) + 1/2 * Q.m * Q.ω^2 * x^2 * ψ x
The Schrodinger operator commutes with the parity operator.
Show Lean code:
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]
4. The eigenfunctions of the Schrodinger Operator
The Physicists Hermite polynomial are defined as polynomials over ℤ in X recursively
with physHermite 0 = 1 and
physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n).
This polynomial will often be cast as a function ℝ → ℝ by evaluating the polynomial at X.
Show Lean code:
noncomputable def physHermite : ℕ → Polynomial ℤ
| 0 => 1
| n + 1 => 2 • X * physHermite n - derivative (physHermite n)
The nth eigenfunction of the Harmonic oscillator is defined as the function ℝ → ℂ
taking x : ℝ to
1/√(2^n n!) 1/√(√π ξ) * physHermite n (x / ξ) * e ^ (- x²/ (2 ξ²)).
Show Lean code:
noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun x =>
1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ)) * physHermite n (x / Q.ξ) *
Real.exp (- x^2 / (2 * Q.ξ^2))
4.1. Properties of the eigenfunctions
The eigenfunctions are integrable.
Show Lean code:
lemma eigenfunction_integrable (n : ℕ) : Integrable (Q.eigenfunction n) := by
rw [eigenfunction_eq]
apply Integrable.const_mul
apply Integrable.ofReal
change Integrable (fun x => physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2)))
have h1 : (fun x => physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2))) =
(fun x => physHermite n (1/Q.ξ * x) * Real.exp (- (1 / (2 * Q.ξ^2)) * x ^ 2)) := by
funext x
ring_nf
rw [h1]
apply guassian_integrable_polynomial_cons
simp
The eigenfunctions are real.
Show Lean code:
lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
(starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x := by
rw [eigenfunction_eq]
simp [-Complex.ofReal_exp]
The eigenfunctions are almost everywhere strongly measurable.
Show Lean code:
lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
(Q.eigenfunction_integrable n).aestronglyMeasurable
The eigenfunctions are square integrable.
Show Lean code:
lemma eigenfunction_square_integrable (n : ℕ) :
MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := by
have h0 (x : ℝ) : Real.exp (- x ^ 2 / Q.ξ^2) =
Real.exp (- (1 /Q.ξ^2) * x ^ 2) := by
simp only [neg_mul, Real.exp_eq_exp]
ring
conv =>
enter [1, x]
rw [eigenfunction_point_norm_sq]
rw [physHermite_pow, h0]
enter [2, 1, 1, 1]
rw [← one_div_mul_eq_div]
apply MeasureTheory.Integrable.const_mul
apply guassian_integrable_polynomial_cons
simp
The eigenfunctions are members of the Hilbert space.
Show Lean code:
lemma eigenfunction_memHS (n : ℕ) : MemHS (Q.eigenfunction n) := by
rw [memHS_iff]
apply And.intro
· fun_prop
· fun_prop
The eigenfunctions are differentiable.
Show Lean code:
lemma eigenfunction_differentiableAt (x : ℝ) (n : ℕ) :
DifferentiableAt ℝ (Q.eigenfunction n) x := by
rw [eigenfunction_eq]
fun_prop
The eigenfunctions are orthonormal within the Hilbert space.
Show Lean code:
lemma eigenfunction_orthonormal :
Orthonormal ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) := by
rw [orthonormal_iff_ite]
intro n p
by_cases hnp : n = p
· simp only [hnp, reduceIte]
exact Q.eigenfunction_normalized p
· simp only [hnp, reduceIte]
exact Q.eigenfunction_orthogonal hnp
The nth eigenfunction is an eigenfunction of the parity operator with
the eigenvalue (-1) ^ n.
Show Lean code:
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 [show -x / Q.ξ = - (x / Q.ξ) by ring]
rw [← physHermite_eq_aeval, physHermite_parity]
simp only [Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_neg, Complex.ofReal_one]
ring_nf
5. The time-independent Schrodinger Equation
The nth eigenvalues for a Harmonic oscillator is defined as (n + 1/2) * ℏ * ω.
Show Lean code:
noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω
The nth eigenfunction satisfies the time-independent Schrodinger equation with
respect to the nth eigenvalue. That is to say for Q a harmonic scillator,
Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x.
The proof of this result is done by explicit calculation of derivatives.
Show Lean code:
lemma schrodingerOperator_eigenfunction (n : ℕ) (x : ℝ) :
Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x := by
simp only [schrodingerOperator_eq_ξ, one_div]
rw [Q.deriv_deriv_eigenfunction]
have hm' := Complex.ofReal_ne_zero.mpr (Ne.symm (_root_.ne_of_lt Q.hm))
have hℏ' := Complex.ofReal_ne_zero.mpr (Ne.symm (_root_.ne_of_lt Q.hℏ))
rw [eigenValue]
simp only [← Complex.ofReal_pow, ξ_sq]
field_simp
ring
6. Completeness
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.
Show Lean code:
lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
(r : ℕ) : ∫ x : ℝ, (x ^ r * (f x * Real.exp (- x^2 / (2 * Q.ξ^2)))) = 0 := by
by_cases hr : r ≠ 0
· have h1 := Q.orthogonal_polynomial_of_mem_orthogonal f hf hOrth (Polynomial.X ^ r)
simp only [map_pow, Polynomial.aeval_X, Complex.ofReal_pow, Complex.ofReal_mul, neg_mul,
Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_ofNat] at h1
have h2 : (fun x => (x /Q.ξ) ^ r *
(f x * Complex.exp (- x ^ 2 / (2 * Q.ξ^2))))
= (fun x => (1/Q.ξ : ℂ) ^ r * (↑x ^r *
(f x * Complex.exp (- x ^ 2 / (2 * Q.ξ^2))))) := by
funext x
ring
rw [h2] at h1
rw [MeasureTheory.integral_mul_left] at h1
simp only [one_div, inv_pow, _root_.mul_eq_zero, inv_eq_zero, pow_eq_zero_iff',
Complex.ofReal_eq_zero, ξ_ne_zero, ne_eq, false_and, false_or] at h1
rw [← h1]
congr
funext x
simp
· simp only [ne_eq, Decidable.not_not] at hr
subst hr
simp only [pow_zero, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, one_mul]
rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth 0]
congr
funext x
simp
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.
Show Lean code:
lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
(c : ℝ) : ∫ x : ℝ, Complex.exp (Complex.I * c * x) *
(f x * Real.exp (- x^2 / (2 * Q.ξ^2))) = 0 := by
/- Rewriting the intergrand as a limit. -/
have h1 (y : ℝ) : Filter.Tendsto (fun n => ∑ r ∈ range n,
(Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))
Filter.atTop (nhds (Complex.exp (Complex.I * c * y) *
(f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by
have h11 : (fun n => ∑ r ∈ range n,
(Complex.I * ↑c * ↑y) ^ r / r !
* (f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) =
fun n => (∑ r ∈ range n,
(Complex.I * ↑c * ↑y) ^ r / r !)
* ((f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) := by
funext s
simp [Finset.sum_mul]
rw [h11]
have h12 : (Complex.exp (Complex.I * c * y) * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))
= (Complex.exp (Complex.I * c * y)) * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))) := by
simp
rw [h12]
apply Filter.Tendsto.mul_const
simp only [Complex.exp, Complex.exp']
haveI hi : CauSeq.IsComplete ℂ norm :=
inferInstanceAs (CauSeq.IsComplete ℂ norm)
exact CauSeq.tendsto_limit (Complex.exp' (Complex.I * c * y))
/- End of rewritting the intergrand as a limit. -/
/- Rewritting the integral as a limit using dominated_convergence -/
have h1' : Filter.Tendsto (fun n => ∫ y : ℝ, ∑ r ∈ range n,
(Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))
Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) *
(f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by
let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * norm (f x) *
(Real.exp (- x ^ 2 / (2 * Q.ξ^2)))
apply MeasureTheory.tendsto_integral_of_dominated_convergence bound
· intro n
apply Finset.aestronglyMeasurable_sum
intro r hr
have h1 : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *
(f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
= fun a => (Complex.I * ↑c) ^ r / ↑r ! *
(f a * Complex.ofReal (a ^ r * (Real.exp (- a ^ 2 / (2 * Q.ξ^2))))) := by
funext a
simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]
ring
rw [h1]
apply MeasureTheory.AEStronglyMeasurable.const_mul
apply MeasureTheory.AEStronglyMeasurable.mul
· exact aeStronglyMeasurable_of_memHS hf
· apply MeasureTheory.Integrable.aestronglyMeasurable
apply MeasureTheory.Integrable.ofReal
change Integrable (fun x => (x ^ r) * (Real.exp (- x ^ 2 / (2 * Q.ξ^2))))
have h1 : (fun x => (x ^ r)*(Real.exp (- x ^ 2 / (2 * Q.ξ^2)))) =
(fun x => (Polynomial.X ^ r : Polynomial ℤ).aeval x *
(Real.exp (- (1/ (2* Q.ξ^2)) * x ^ 2))) := by
funext x
simp only [neg_mul, map_pow, Polynomial.aeval_X, mul_eq_mul_left_iff, Real.exp_eq_exp,
pow_eq_zero_iff', ne_eq]
left
field_simp
rw [h1]
apply guassian_integrable_polynomial
simp
· /- Prove the bound is integrable. -/
have hbound : bound = (fun x => Real.exp |c * x| * norm (f x) *
Real.exp (-(1/ (2 * Q.ξ^2)) * x ^ 2)) := by
simp only [neg_mul, bound]
funext x
congr
field_simp
rw [hbound]
apply HilbertSpace.exp_abs_mul_abs_mul_gaussian_integrable
· exact hf
· simp
· intro n
apply Filter.Eventually.of_forall
intro y
rw [← Finset.sum_mul]
simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, norm_mul,
bound]
rw [mul_assoc]
conv_rhs =>
rw [mul_assoc]
have h1 : (norm (f y) * norm (Complex.exp (-(↑y ^ 2) / (2 * Q.ξ^2))))
= norm (f y) * Real.exp (-(y ^ 2) / (2 * Q.ξ^2)) := by
simp only [mul_eq_mul_left_iff, map_eq_zero, bound]
left
rw [Complex.norm_exp]
congr
trans (Complex.ofReal (- y ^ 2 / (2 * Q.ξ^2))).re
· congr
simp
· rw [Complex.ofReal_re]
rw [h1]
by_cases hf : norm (f y) = 0
· simp [hf]
rw [_root_.mul_le_mul_right]
· have h1 := Real.sum_le_exp_of_nonneg (x := |c * y|) (abs_nonneg (c * y)) n
refine le_trans ?_ h1
have h2 : norm (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤
∑ i ∈ range n, norm ((Complex.I * (↑c * ↑y)) ^ i / ↑i !) := by
exact norm_sum_le _ _
refine le_trans h2 ?_
apply le_of_eq
congr
funext i
simp only [Complex.norm_div, norm_pow, Complex.norm_mul, Complex.norm_I, Complex.norm_real,
Real.norm_eq_abs, one_mul, RCLike.norm_natCast, bound]
congr
rw [abs_mul]
· refine mul_pos ?_ ?_
have h1 : 0 ≤ norm (f y) := norm_nonneg (f y)
apply lt_of_le_of_ne h1 (fun a => hf (id (Eq.symm a)))
exact Real.exp_pos (- y ^ 2 / (2 * Q.ξ^2))
· apply Filter.Eventually.of_forall
intro y
exact h1 y
have h3b : (fun n => ∫ y : ℝ, ∑ r ∈ range n,
(Complex.I * ↑c * ↑y) ^ r / r ! *
(f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) = fun (n : ℕ) => 0 := by
funext n
rw [MeasureTheory.integral_finset_sum]
· apply Finset.sum_eq_zero
intro r hr
have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *
(f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
= fun a => ((Complex.I * ↑c) ^ r / ↑r !) *
(a^ r * (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2))))) := by
funext a
simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]
ring
rw [hf']
rw [MeasureTheory.integral_mul_left]
rw [Q.orthogonal_power_of_mem_orthogonal f hf hOrth r]
simp
· intro r hr
have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *
(f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
= ((Complex.I * ↑c) ^ r / ↑r !) •
fun a => (a^ r * (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2))))) := by
funext a
simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, Pi.smul_apply, smul_eq_mul]
ring
rw [hf']
apply MeasureTheory.Integrable.smul
exact Q.mul_power_integrable f hf r
rw [h3b] at h1'
apply tendsto_nhds_unique h1'
rw [tendsto_const_nhds_iff]
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.
Show Lean code:
lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) :
𝓕 (fun x => f x * Real.exp (- x^2 / (2 * Q.ξ^2))) = 0 := by
funext c
rw [Real.fourierIntegral_eq]
simp only [RCLike.inner_apply, conj_trivial, neg_mul, ofReal_exp, ofReal_div, ofReal_neg,
ofReal_mul, ofReal_pow, ofReal_ofNat, Pi.zero_apply]
rw [← Q.orthogonal_exp_of_mem_orthogonal f hf hOrth (- 2 * Real.pi * c)]
congr
funext x
simp only [fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul, ofReal_ofNat,
AddChar.coe_mk, ofReal_neg, mul_neg, neg_mul, ofReal_exp, ofReal_div, ofReal_pow]
change Complex.exp (-(2 * ↑Real.pi * (x * c) * Complex.I)) *
(f x * Complex.exp (- x ^ 2 / (2 * Q.ξ^2))) = _
congr 2
ring
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.
Show Lean code:
theorem eigenfunction_completeness
(plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : MemLp f 2),
eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) :
(Submodule.span ℂ
(Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)))).topologicalClosure = ⊤ := by
rw [Submodule.topologicalClosure_eq_top_iff]
refine (Submodule.eq_bot_iff (Submodule.span ℂ
(Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n))))ᗮ).mpr ?_
intro f hf
apply Q.zero_of_orthogonal_eigenVector f ?_ plancherel_theorem
intro n
rw [@Submodule.mem_orthogonal'] at hf
rw [← inner_conj_symm]
have hl : ⟪f, HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 0 := by
apply hf
refine Finsupp.mem_span_range_iff_exists_finsupp.mpr ?_
use Finsupp.single n 1
simp
rw [hl]
simp