Merge pull request #347 from HEPLean/JTS/QuantumMechanics

feat: Completeness of eigenvectors for harmonic oscillator

PhysLean.lean

@@ -181,8 +181,11 @@ import PhysLean.PerturbationTheory.WickContraction.TimeCond
 import PhysLean.PerturbationTheory.WickContraction.TimeContract
 import PhysLean.PerturbationTheory.WickContraction.Uncontracted
 import PhysLean.PerturbationTheory.WickContraction.UncontractedList
-import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator
-import PhysLean.QuantumMechanics.OneDimension.HilbertSpace
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
+import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
 import PhysLean.SpaceTime.Basic
 import PhysLean.SpaceTime.CliffordAlgebra
 import PhysLean.StandardModel.Basic

PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean

@@ -5,6 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
 import Mathlib.Analysis.Calculus.Deriv.Polynomial
 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
 /-!
 
 # Physicists Hermite Polynomial
@@ -129,13 +130,26 @@ lemma iterate_derivative_physHermite_self {n : ℕ} :
     rw [Polynomial.coeff_C_ne_zero (by omega)]
     rfl
 
+@[simp]
+lemma physHermite_leadingCoeff {n : ℕ} : (physHermite n).leadingCoeff = 2 ^ n := by
+  simp [leadingCoeff]
+
+@[simp]
+lemma physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0 := by
+  refine leadingCoeff_ne_zero.mp ?_
+  simp
+
 /-- The physicists Hermite polynomial as a function from `ℝ` to `ℝ`. -/
 noncomputable def physHermiteFun (n : ℕ) : ℝ → ℝ := fun x => aeval x (physHermite n)
 
 @[simp]
 lemma physHermiteFun_zero_apply (x : ℝ) : physHermiteFun 0 x = 1 := by
   simp [physHermiteFun, aeval]
 
+lemma physHermiteFun_pow (n m : ℕ) (x : ℝ) :
+    physHermiteFun n x ^ m = aeval x (physHermite n ^ m) := by
+  simp [physHermiteFun]
+
 lemma physHermiteFun_eq_aeval_physHermite (n : ℕ) :
     physHermiteFun n = fun x => aeval x (physHermite n) := rfl
 
@@ -441,4 +455,110 @@ lemma physHermiteFun_norm_cons (n : ℕ) (c : ℝ) :
     (fun x => physHermiteFun n x * physHermiteFun n x * Real.exp (-x ^ 2)) c]
   rw [physHermiteFun_norm]
 
+lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : ℕ) →
+    (hn : P.natDegree = n) →
+    (fun x => P.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun)
+  | 0, h => by
+    rw [natDegree_eq_zero] at h
+    obtain ⟨x, rfl⟩ := h
+    refine Finsupp.mem_span_range_iff_exists_finsupp.mpr ?_
+    use Finsupp.single 0 x
+    funext y
+    simp
+  | n + 1, h => by
+    by_cases hP0 : P = 0
+    · subst hP0
+      simp only [map_zero]
+      change 0 ∈ _
+      exact Submodule.zero_mem (Submodule.span ℝ (Set.range physHermiteFun))
+    let P' := ((coeff (physHermite (n + 1)) (n + 1)) • P -
+        (coeff P (n + 1)) • physHermite (n + 1))
+    have hP'mem : (fun x => P'.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun) := by
+      by_cases hP' : P' = 0
+      · rw [hP']
+        simp only [map_zero]
+        change 0 ∈ _
+        exact Submodule.zero_mem (Submodule.span ℝ (Set.range physHermiteFun))
+      · exact polynomial_mem_physHermiteFun_span_induction P' P'.natDegree (by rfl)
+    simp only [P'] at hP'mem
+    have hl : (fun x => (aeval x) ((physHermite (n + 1)).coeff (n + 1) • P -
+        P.coeff (n + 1) • physHermite (n + 1)))
+        = (2 ^ (n + 1) : ℝ) • (fun (x : ℝ) => (aeval x) P) - ↑(P.coeff (n + 1) : ℝ) •
+        (fun (x : ℝ)=> (aeval x) (physHermite (n + 1))) := by
+      funext x
+      simp only [coeff_physHermite_self_succ, zsmul_eq_mul, Int.cast_pow, Int.cast_ofNat, map_sub,
+        map_mul, map_pow, map_intCast, Pi.sub_apply, Pi.smul_apply, smul_eq_mul, sub_left_inj,
+        mul_eq_mul_right_iff, P']
+      simp [aeval]
+    rw [hl] at hP'mem
+    rw [Submodule.sub_mem_iff_left] at hP'mem
+    rw [Submodule.smul_mem_iff] at hP'mem
+    exact hP'mem
+    simp only [ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
+      pow_eq_zero_iff, OfNat.ofNat_ne_zero, P']
+    apply Submodule.smul_mem _
+    refine Finsupp.mem_span_range_iff_exists_finsupp.mpr ?_
+    use Finsupp.single (n + 1) 1
+    simp
+    rfl
+decreasing_by
+  rw [Polynomial.natDegree_lt_iff_degree_lt]
+  apply (Polynomial.degree_lt_iff_coeff_zero _ _).mpr
+  intro m hm'
+  simp only [coeff_physHermite_self_succ, Int.cast_pow, Int.cast_ofNat, coeff_sub,
+      Int.cast_id]
+  change n + 1 ≤ m at hm'
+  rw [coeff_smul, coeff_smul]
+  by_cases hm : m = n + 1
+  · subst hm
+    simp only [smul_eq_mul, coeff_physHermite_self_succ]
+    ring
+  · rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt (n := m)]
+    simp only [smul_eq_mul, mul_zero, sub_self]
+    · rw [← Polynomial.natDegree_lt_iff_degree_lt]
+      simp only [natDegree_physHermite]
+      omega
+      simp
+    · rw [← Polynomial.natDegree_lt_iff_degree_lt]
+      omega
+      exact hP0
+  · exact hP'
+
+lemma polynomial_mem_physHermiteFun_span (P : Polynomial ℤ) :
+    (fun x => P.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun) := by
+  exact polynomial_mem_physHermiteFun_span_induction P P.natDegree rfl
+
+lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) :
+    (fun (x : ℝ) => Real.cos (c * x)) ∈
+    (Submodule.span ℝ (Set.range physHermiteFun)).topologicalClosure := by
+  change (fun (x : ℝ) => Real.cos (c * x)) ∈
+    closure (Submodule.span ℝ (Set.range physHermiteFun))
+  have h1 := Real.hasSum_cos
+  simp [HasSum] at h1
+  have h1 : Filter.Tendsto
+      (fun s => fun y => ∑ x ∈ s, (-1) ^ x * (c * y) ^ (2 * x) / ((2 * x)! : ℝ))
+    Filter.atTop (nhds (fun x => Real.cos (c * x))) := by
+    exact tendsto_pi_nhds.mpr fun x => h1 (c * x)
+  have h2 (z : Finset ℕ) : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) ∈
+      ↑(Submodule.span ℝ (Set.range physHermiteFun)) := by
+    have h0 : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) =
+      ∑ x ∈ z, (((-1) ^ x * c ^ (2 * x) / ↑(2 * x)!) • fun (y : ℝ) => (y) ^ (2 * x)) := by
+      funext y
+      simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+      congr
+      funext z
+      ring
+    rw [h0]
+    apply Submodule.sum_mem
+    intro l hl
+    apply Submodule.smul_mem
+    let P : Polynomial ℤ := X ^ (2 * l)
+    have hy : (fun y => y ^ (2 * l)) = (fun (y : ℝ) => P.aeval y) := by
+      funext y
+      simp [P]
+    rw [hy]
+    exact polynomial_mem_physHermiteFun_span P
+  refine mem_closure_of_tendsto h1 ?_
+  simp [h2]
+
 end PhysLean