refactor: rename top level directories

docs/_data/harmonicOscillator.yml

@@ -0,0 +1,714 @@
+
+title: "The Quantum Harmonic Oscillator in Lean 4"
+curators: Joseph Tooby-Smith
+parts:
+  
+  - type: h1
+    sectionNo: 1
+    content: "Introduction"
+
+  - type: p
+    content: "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."
+
+  - type: p
+    content: " 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 <a href = 'https://heplean.com'>here</a>."
+
+  - type: p
+    content: "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."
+
+  - type: h1
+    sectionNo: 2
+    content: "Hilbert Space"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HilbertSpace
+    line: 26
+    fileName: PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean#L26"
+    isDef: true
+    isThm: false
+    docString: |
+      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 `ℂ`. 
+    declString: |
+      noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2
+    declNo: "2.1"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HilbertSpace.MemHS
+    line: 34
+    fileName: PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean#L34"
+    isDef: true
+    isThm: false
+    docString: |
+      The proposition `MemHS f` for a function `f : ℝ → ℂ` is defined
+      to be true if the function `f` can be lifted to the Hilbert space. 
+    declString: |
+      def MemHS (f : ℝ → ℂ) : Prop := Memℒp f 2 MeasureTheory.volume
+    declNo: "2.2"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HilbertSpace.memHS_iff
+    line: 42
+    fileName: PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean#L42"
+    isDef: false
+    isThm: false
+    docString: |
+      A function `f` statisfies `MemHS f` if and only if it is almost everywhere
+      strongly measurable, and square integrable. 
+    declString: |
+      lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
+          AEStronglyMeasurable f ∧ Integrable (fun x => ‖f x‖ ^ 2) := by
+        rw [MemHS]
+        simp only [Memℒp, Complex.norm_eq_abs, and_congr_right_iff]
+        intro h1
+        rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_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 => Complex.abs (f x) ^ 2) MeasureTheory.volume := by
+          apply MeasureTheory.AEStronglyMeasurable.pow
+          exact Continuous.comp_aestronglyMeasurable Complex.continuous_abs h1
+        simp only [h0, true_and]
+        simp only [HasFiniteIntegral, enorm_pow]
+        simp only [enorm, nnnorm, Complex.norm_eq_abs, Real.norm_eq_abs, Complex.abs_abs]
+    declNo: "2.3"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HilbertSpace.mk
+    line: 67
+    fileName: PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean#L67"
+    isDef: true
+    isThm: false
+    docString: |
+      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`. 
+    declString: |
+      def mk {f : ℝ → ℂ} (hf : MemHS f) : HilbertSpace :=
+        ⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩
+    declNo: "2.4"
+
+  - type: h1
+    sectionNo: 3
+    content: "The Schrodinger Operator"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator
+    line: 57
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean#L57"
+    isDef: true
+    isThm: false
+    docString: |
+      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. 
+    declString: |
+      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
+    declNo: "3.1"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator
+    line: 98
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean#L98"
+    isDef: true
+    isThm: false
+    docString: |
+      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 * ψ`. 
+    declString: |
+      noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
+        fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y
+    declNo: "3.2"
+
+  - type: h1
+    sectionNo: 4
+    content: "The eigenfunctions of the Schrodinger Operator"
+
+  - type: name
+    name: PhysLean.physHermite
+    line: 20
+    fileName: PhysLean.Mathematics.SpecialFunctions.PhyscisistsHermite
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean#L20"
+    isDef: true
+    isThm: false
+    docString: |
+      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`.
+      
+    declString: |
+      noncomputable def physHermite : ℕ → Polynomial ℤ
+        | 0 => 1
+        | n + 1 => 2 • X * physHermite n - derivative (physHermite n)
+    declNo: "4.1"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction
+    line: 24
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L24"
+    isDef: true
+    isThm: false
+    docString: |
+      The `n`th  eigenfunction of the Harmonic oscillator is defined as the function `ℝ → ℂ`
+      taking `x : ℝ` to
+      
+      `1/√(2^n n!) (m ω /(π ℏ))^(1/4) * physHermite n (√(m ω /ℏ) x) * e ^ (- m ω x^2/2ℏ)`.
+      
+      
+    declString: |
+      noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun x =>
+        1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+        physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))
+    declNo: "4.2"
+
+  - type: h2
+    sectionNo: "4.1"
+    content: "Properties of the eigenfunctions"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable
+    line: 77
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L77"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are integrable. 
+    declString: |
+      lemma eigenfunction_integrable (n : ℕ) : MeasureTheory.Integrable (Q.eigenfunction n) := by
+        rw [eigenfunction_eq]
+        apply MeasureTheory.Integrable.const_mul
+        apply MeasureTheory.Integrable.ofReal
+        change MeasureTheory.Integrable
+          (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+          (Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) MeasureTheory.volume
+        have h1 : (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+            (Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) =
+            (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+            (Real.exp (- (Q.m * Q.ω / (2* Q.ℏ)) * x ^ 2))) := by
+          funext x
+          simp only [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp]
+          left
+          field_simp
+        rw [h1]
+        apply guassian_integrable_polynomial_cons
+        simp
+    declNo: "4.3"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj
+    line: 98
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L98"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are real. 
+    declString: |
+      lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
+          (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x := by
+        rw [eigenfunction_eq]
+        simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
+          neg_mul, map_mul, map_inv₀, Complex.conj_ofReal]
+    declNo: "4.4"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable
+    line: 157
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L157"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are almost everywhere strongly measurable. 
+    declString: |
+      lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
+          MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
+        (Q.eigenfunction_integrable n).aestronglyMeasurable
+    declNo: "4.5"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable
+    line: 141
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L141"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are square integrable. 
+    declString: |
+      lemma eigenfunction_square_integrable (n : ℕ) :
+          MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := by
+        have h0 (x : ℝ) : Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ) =
+            Real.exp (- (Q.m * Q.ω /Q.ℏ) * 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]
+        apply MeasureTheory.Integrable.const_mul
+        apply guassian_integrable_polynomial_cons
+        simp
+    declNo: "4.6"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS
+    line: 163
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L163"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are members of the Hilbert space. 
+    declString: |
+      lemma eigenfunction_memHS (n : ℕ) : MemHS (Q.eigenfunction n) := by
+        rw [memHS_iff]
+        apply And.intro
+        · fun_prop
+        · fun_prop
+    declNo: "4.7"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt
+    line: 170
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L170"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are differentiable. 
+    declString: |
+      lemma eigenfunction_differentiableAt (x : ℝ) (n : ℕ) :
+          DifferentiableAt ℝ (Q.eigenfunction n) x := by
+        rw [eigenfunction_eq]
+        fun_prop
+    declNo: "4.8"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal
+    line: 383
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean#L383"
+    isDef: false
+    isThm: false
+    docString: |
+      The eigenfunctions are orthonormal within the Hilbert space. 
+    declString: |
+      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
+    declNo: "4.9"
+
+  - type: h1
+    sectionNo: 5
+    content: "The time-independent Schrodinger Equation"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue
+    line: 24
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean#L24"
+    isDef: true
+    isThm: false
+    docString: |
+      The `n`th eigenvalues for a Harmonic oscillator is defined as `(n + 1/2) * ℏ * ω`. 
+    declString: |
+      noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω
+    declNo: "5.1"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction
+    line: 262
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean#L262"
+    isDef: false
+    isThm: true
+    docString: |
+      The `n`th eigenfunction satisfies the time-independent Schrodinger equation with
+      respect to the `n`th 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.
+      
+    declString: |
+      theorem schrodingerOperator_eigenfunction (n : ℕ) :
+          Q.schrodingerOperator (Q.eigenfunction n) x =
+          Q.eigenValue n * Q.eigenfunction n x :=
+        match n with
+        | 0 => Q.schrodingerOperator_eigenfunction_zero x
+        | 1 => Q.schrodingerOperator_eigenfunction_one x
+        | n + 2 => Q.schrodingerOperator_eigenfunction_succ_succ n x
+    declNo: "5.2"
+
+  - type: h1
+    sectionNo: 6
+    content: "Completeness"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_power_of_mem_orthogonal
+    line: 260
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean#L260"
+    isDef: false
+    isThm: false
+    docString: |
+      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 ^ (- m ω x ^ 2 / (2 ℏ))`
+      
+      the proof of this result relies on the fact that Hermite polynomials span polynomials. 
+    declString: |
+      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 (- m * ω * x^2 / (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 => (↑√(m * ω / ℏ) * ↑x) ^ r *
+            (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ))))
+            = (fun x => (↑√(m * ω / ℏ) : ℂ) ^ r * (↑x ^r *
+            (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ))))) := by
+            funext x
+            ring
+          rw [h2] at h1
+          rw [MeasureTheory.integral_mul_left] at h1
+          simp only [_root_.mul_eq_zero, pow_eq_zero_iff', Complex.ofReal_eq_zero, ne_eq] at h1
+          have h0 : r ≠ 0 := by
+            exact hr
+          have h0' : √(m * ω / (ℏ)) ≠ 0 := by
+            simp only [ne_eq]
+            refine Real.sqrt_ne_zero'.mpr ?_
+            refine div_pos ?_ ?_
+            · exact mul_pos hm hω
+            · exact hℏ
+          simp only [h0', h0, not_false_eq_true, and_true, 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
+    declNo: "6.1"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_exp_of_mem_orthogonal
+    line: 307
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean#L307"
+    isDef: false
+    isThm: false
+    docString: |
+      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 ^ (- m ω x ^ 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. 
+    declString: |
+      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 (- m * ω * x^2 / (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 (- m * ω * y^2 / (2 * ℏ))))
+            Filter.atTop (nhds (Complex.exp (Complex.I * c * y) *
+            (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by
+          have h11 : (fun n => ∑ r ∈ range n,
+              (Complex.I * ↑c * ↑y) ^ r / r !
+              * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) =
+              fun n => (∑ r ∈ range n,
+              (Complex.I * ↑c * ↑y) ^ r / r !)
+              * ((f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) := by
+            funext s
+            simp [Finset.sum_mul]
+          rw [h11]
+          have h12 : (Complex.exp (Complex.I * c * y) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))
+            = (Complex.exp (Complex.I * c * y)) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))) := by
+            simp
+          rw [h12]
+          apply Filter.Tendsto.mul_const
+          simp only [Complex.exp, Complex.exp']
+          haveI hi : CauSeq.IsComplete ℂ norm :=
+            inferInstanceAs (CauSeq.IsComplete ℂ Complex.abs)
+          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 (- m * ω * y^2 / (2 * ℏ))))
+            Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) *
+            (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by
+          let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * Complex.abs (f x) *
+            (Real.exp (-m * ω * x ^ 2 / (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 (-m * ω * a ^ 2 / (2 * ℏ)))))
+              = fun a => (Complex.I * ↑c) ^ r / ↑r ! *
+              (f a * Complex.ofReal (a ^ r * (Real.exp (-m * ω * a ^ 2 / (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 (-m * ω * x ^ 2 / (2 * ℏ))))
+              have h1 : (fun x => (x ^ r)*(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) =
+                  (fun x => (Polynomial.X ^ r : Polynomial ℤ).aeval x *
+                  (Real.exp (- (m * ω / (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| * Complex.abs (f x) *
+                Real.exp (-(m * ω / (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
+            · refine div_pos ?_ ?_
+              · exact mul_pos hm hω
+              · have h1 := Q.hℏ
+                linarith
+          · 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, Complex.norm_eq_abs,
+              bound]
+            rw [mul_assoc]
+            conv_rhs =>
+              rw [mul_assoc]
+            have h1 : (Complex.abs (f y) * Complex.abs (Complex.exp (-(↑m * ↑ω * ↑y ^ 2) / (2 * ↑ℏ))))
+              = Complex.abs (f y) * Real.exp (-(m * ω * y ^ 2) / (2 * ℏ)) := by
+              simp only [mul_eq_mul_left_iff, map_eq_zero, bound]
+              left
+              rw [Complex.abs_exp]
+              congr
+              trans (Complex.ofReal (-(m * ω * y ^ 2) / (2 * ℏ))).re
+              · congr
+                simp
+              · rw [Complex.ofReal_re]
+            rw [h1]
+            by_cases hf : Complex.abs (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 : Complex.abs (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤
+                ∑ i ∈ range n, Complex.abs ((Complex.I * (↑c * ↑y)) ^ i / ↑i !) := by
+                exact AbsoluteValue.sum_le _ _ _
+              refine le_trans h2 ?_
+              apply le_of_eq
+              congr
+              funext i
+              simp only [map_div₀, AbsoluteValue.map_pow, AbsoluteValue.map_mul, Complex.abs_I,
+                Complex.abs_ofReal, one_mul, Complex.abs_natCast, bound]
+              congr
+              rw [abs_mul]
+            · refine mul_pos ?_ ?_
+              have h1 : 0 ≤ Complex.abs (f y) := by exact AbsoluteValue.nonneg Complex.abs (f y)
+              apply lt_of_le_of_ne h1 (fun a => hf (id (Eq.symm a)))
+              exact Real.exp_pos (-(m * ω * y ^ 2) / (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 (- m * ω * y^2 / (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 (-m * ω * a ^ 2 / (2 * ℏ)))))
+              = fun a => ((Complex.I * ↑c) ^ r / ↑r !) *
+              (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (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 (-m * ω * a ^ 2 / (2 * ℏ)))))
+              = ((Complex.I * ↑c) ^ r / ↑r !) •
+              fun a => (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (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]
+    declNo: "6.2"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.fourierIntegral_zero_of_mem_orthogonal
+    line: 477
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean#L477"
+    isDef: false
+    isThm: false
+    docString: |
+      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 ^ (- m ω x ^ 2 / (2 ℏ))`
+      
+      is zero.
+      
+      The proof of this result relies on `orthogonal_exp_of_mem_orthogonal`. 
+    declString: |
+      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 (- m * ω * x^2 / (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 (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ))) = _
+        congr 2
+        ring
+    declNo: "6.3"
+
+  - type: name
+    name: QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness
+    line: 564
+    fileName: PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+    status: "complete"
+    link: "https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean#L564"
+    isDef: false
+    isThm: true
+    docString: |
+      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 ^ (- m * ω * x^2 / (2 * ℏ)`
+      
+      is zero for `f` orthogonal to all eigenfunctions, and hence the norm of `f` is zero.
+      
+    declString: |
+      theorem eigenfunction_completeness
+          (plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp 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
+    declNo: "6.4"