Merge pull request #355 from HEPLean/JTS/QuantumMechanics

refactor: Golf QM proofs
HEPLean · Feb 27, 2025 · 7044812 · 7044812
2 parents 5a65b38 + db13669
commit 7044812
Show file tree

Hide file tree

Showing 4 changed files with 103 additions and 157 deletions.
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
@@ -96,12 +96,40 @@ lemma ℏ_ne_zero : Q.ℏ ≠ 0 := by
   have h1 := Q.hℏ
   linarith
 
+/-- The characteristic length of the harmonic oscilator.
+  Defined as `√(ℏ /(m ω))`. -/
+noncomputable def ξ : ℝ := √(Q.ℏ / (Q.m * Q.ω))
+
+lemma ξ_nonneg : 0 ≤ Q.ξ := Real.sqrt_nonneg _
+
+lemma ξ_pos : 0 < Q.ξ := by
+  rw [ξ]
+  apply Real.sqrt_pos.mpr
+  apply div_pos
+  · exact Q.hℏ
+  · exact mul_pos Q.hm Q.hω
+
+@[simp]
+lemma ξ_abs : abs Q.ξ = Q.ξ := abs_of_nonneg Q.ξ_nonneg
+
+lemma one_over_ξ : 1/Q.ξ = √(Q.m * Q.ω / Q.ℏ) := by
+  have := Q.hℏ
+  field_simp [ξ]
+
+lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ):= by
+  rw [inv_eq_one_div]
+  exact one_over_ξ Q
+
+lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / Q.ℏ := by
+  rw [one_over_ξ]
+  refine Real.sq_sqrt (le_of_lt Q.m_mul_ω_div_ℏ_pos)
+
 /-- 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 * ψ`. -/
 noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
-  fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y
+  fun x => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) x) + 1/2 * Q.m * Q.ω^2 * x^2 * ψ x
 
 open HilbertSpace
 

diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
@@ -167,8 +167,7 @@ local notation "hω" => Q.hω
 
 lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
-    (n : ℕ) :
-    ∫ (x : ℝ), (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    (n : ℕ) : ∫ (x : ℝ), (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
     = 0 := by
   have h1 := Q.orthogonal_eigenfunction_of_mem_orthogonal f hf hOrth n
@@ -208,8 +207,7 @@ lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
 lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (P : Polynomial ℤ) :
-    ∫ x : ℝ, (P (√(m * ω / ℏ) * x)) *
-      (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by
+    ∫ x : ℝ, (P (√(m * ω / ℏ) * x)) * (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by
   have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1

diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
@@ -29,13 +29,12 @@ open HilbertSpace
 
 -/
 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.ℏ))
+  1/√(2 ^ n * n !) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ)) *
+  physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))
 
 lemma eigenfunction_eq (n : ℕ) :
-    Q.eigenfunction n = fun (x : ℝ) =>
-    ((1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-    Complex.ofReal (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) *
+    Q.eigenfunction n = fun (x : ℝ) => ((1/√(2 ^ n * n !) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+    Complex.ofReal (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) *
     Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by
   funext x
   simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div,
@@ -44,30 +43,20 @@ lemma eigenfunction_eq (n : ℕ) :
   ring
 
 lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) =>
-    (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
-    Complex.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
+    √√(Q.m * Q.ω / (Real.pi * Q.ℏ)) * Complex.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) := by
   funext x
   simp [eigenfunction]
 
 lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
-    Q.eigenfunction n = fun x => Complex.ofReal (1/Real.sqrt (2 ^ n * n !))
-    * Complex.ofReal (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))
-    * Q.eigenfunction 0 x := by
+    Q.eigenfunction n = fun x => Complex.ofReal (1/√(2 ^ n * n !))
+    * Complex.ofReal (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) * Q.eigenfunction 0 x := by
   match n with
   | 0 =>
     simp
   | n + 1 =>
     funext x
-    rw [eigenfunction, eigenfunction_zero]
-    repeat rw [mul_assoc]
-    congr 1
-    · simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
-        Complex.ofReal_inv]
-    · rw [mul_comm, mul_assoc]
-      congr 1
-      simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
-        Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]
-      ring_nf
+    field_simp [eigenfunction, eigenfunction_zero]
+    ring
 
 /-!
 
@@ -104,10 +93,8 @@ lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
   simp [-Complex.ofReal_exp]
 
 lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
-    ‖Q.eigenfunction n 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.ℏ))) := by
+    ‖Q.eigenfunction n x‖ = (1/√(2 ^ n * n !) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+    (|physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)| * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))) := by
   rw [eigenfunction_eq]
   simp only [neg_mul, Complex.ofReal_mul, Complex.norm_eq_abs]
   rw [AbsoluteValue.map_mul, AbsoluteValue.map_mul]
@@ -121,14 +108,11 @@ lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
       simp [abs_of_nonneg]
 
 lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) :
-    ‖Q.eigenfunction n x‖ ^ 2 = (1/Real.sqrt (2 ^ n * n !) *
-    Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 *
-    ((physHermite n
-    (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) ^ 2 * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
-  trans (1/Real.sqrt (2 ^ n * n !) *
-    Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 *
-    ((|physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)|) ^ 2 *
-    (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) ^ (2 : ℝ)))
+    ‖Q.eigenfunction n x‖ ^ 2 = (1/√(2 ^ n * n !) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) ^ 2 *
+    ((physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) ^ 2 * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
+  trans (1/√(2 ^ n * n !) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) ^ 2 *
+    ((|physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)|) ^ 2 *
+    Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) ^ (2 : ℝ))
   · simp only [Real.rpow_two]
     rw [eigenfunction_point_norm]
     ring
@@ -201,26 +185,21 @@ lemma eigenfunction_parity (n : ℕ) :
 /-- A simplification of the product of two eigen-functions. -/
 lemma eigenfunction_mul (n p : ℕ) :
     (Q.eigenfunction n x) * (Q.eigenfunction p x) =
-    ((1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
-    ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))))) *
-    Complex.ofReal ((physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-    physHermite p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) * (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ))) := by
+    1/√(2 ^ n * n !) * 1/√(2 ^ p * p !) * √(Q.m * Q.ω / (Real.pi * Q.ℏ)) *
+    Complex.ofReal (physHermite n (√(Q.m * Q.ω /Q.ℏ) * x) *
+    physHermite p (√(Q.m * Q.ω /Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
   calc Q.eigenfunction n x * Q.eigenfunction p x
-    _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
-      (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
-      Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-        physHermite p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) *
-      (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
+    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) *
+        (√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+        (physHermite n (√(Q.m * Q.ω /Q.ℏ) * x) * physHermite p (√(Q.m * Q.ω /Q.ℏ) * x)) *
+        (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
       simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
         one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
         Complex.ofReal_pow, Complex.ofReal_ofNat, mul_one]
       ring
-    _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
-      ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-        physHermite p (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) *
-      (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
+    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * √(Q.m * Q.ω / (Real.pi * Q.ℏ)) *
+        (physHermite n (√(Q.m * Q.ω /Q.ℏ) * x) *  physHermite p (√(Q.m * Q.ω / Q.ℏ) * x)) *
+        (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
       congr 1
       · congr 1
         · congr 1
@@ -239,25 +218,21 @@ lemma eigenfunction_mul (n p : ℕ) :
     Complex.ofReal_pow]
   ring
 
-lemma eigenfunction_mul_self (n : ℕ) :
-    (Q.eigenfunction n x) * (Q.eigenfunction n x) =
-    ((1/ (2 ^ n * n !)) * (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-    Complex.ofReal ((physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
-    (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ))) := by
+lemma eigenfunction_mul_self (n : ℕ) : (Q.eigenfunction n x) * (Q.eigenfunction n x) =
+    (1/ (2 ^ n * n !) * √(Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+    Complex.ofReal ((physHermite n (√(Q.m * Q.ω /Q.ℏ) * x))^2 *
+    Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
   calc Q.eigenfunction n x * Q.eigenfunction n x
-    _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ n * n !)) *
-      (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
-      Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
-      (Real.exp (-Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
+    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ n * n !)) *
+        (√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) * √√(Q.m * Q.ω / (Real.pi * Q.ℏ))) *
+        (physHermite n (√(Q.m * Q.ω /Q.ℏ) * x))^2 *
+        (Real.exp (-Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
       simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
         one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
         Complex.ofReal_pow, Complex.ofReal_ofNat, mul_one]
       ring
-    _ = (1/ (2 ^ n * n !)) *
-      ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))^2 *
-      (Real.exp (- Q.m * Q.ω * x^2 /Q.ℏ)) := by
+    _ = (1/ (2 ^ n * n !)) * √(Q.m * Q.ω / (Real.pi * Q.ℏ)) *
+        (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))^2 * Real.exp (- Q.m * Q.ω * x^2 /Q.ℏ) := by
       congr 1
       · congr 1
         · congr 1
@@ -288,83 +263,38 @@ lemma eigenfunction_mul_self (n : ℕ) :
 open InnerProductSpace
 
 /-- The eigenfunction are normalized. -/
-lemma eigenfunction_normalized (n : ℕ) :
-    ⟪HilbertSpace.mk (Q.eigenfunction_memHS n),
-      HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := by
+lemma eigenfunction_normalized (n : ℕ) : ⟪HilbertSpace.mk (Q.eigenfunction_memHS n),
+    HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := by
   rw [inner_mk_mk]
   conv_lhs =>
     enter [2, x]
     rw [eigenfunction_conj, Q.eigenfunction_mul_self]
   rw [MeasureTheory.integral_mul_left, integral_complex_ofReal]
-  let c := √(Q.m * Q.ω / Q.ℏ)
-  have h1 : c ^ 2 = Q.m * Q.ω / Q.ℏ := by
-    trans c * c
-    · exact pow_two c
-    simp only [c]
-    refine Real.mul_self_sqrt ?_
-    refine div_nonneg ?_ ?_
-    exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
-    exact le_of_lt Q.hℏ
   have hc : (∫ (x : ℝ), physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 *
       Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ))
-      = ∫ (x : ℝ), (physHermite n (c * x) *
-      physHermite n (c * x)) * Real.exp (- c^2 * x ^ 2) := by
+      = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) *
+      physHermite n (1/Q.ξ * x)) * Real.exp (- (1/Q.ξ)^2 * x ^ 2) := by
     congr
     funext x
     congr
-    · simp only [c]
+    · simp only [one_over_ξ]
       exact pow_two _
-    simp only [neg_mul, h1, c]
-    field_simp
+    · simp only [neg_mul, one_over_ξ_sq]
+      field_simp
   rw [hc, physHermite_norm_cons]
   simp only [one_div, mul_inv_rev, smul_eq_mul, Complex.ofReal_mul, Complex.ofReal_natCast,
-    Complex.ofReal_pow, Complex.ofReal_ofNat, c]
+    Complex.ofReal_pow, Complex.ofReal_ofNat]
   ring_nf
-  have h1 : ↑n ! * (↑n ! : ℂ)⁻¹ = 1 := by
-    rw [← IsUnit.eq_mul_inv_iff_mul_eq]
-    simp only [inv_inv, one_mul, c]
-    refine IsUnit.inv ?_
-    simp only [isUnit_iff_ne_zero, ne_eq, cast_eq_zero, c]
-    exact factorial_ne_zero n
-  rw [h1]
-  repeat rw [mul_assoc]
-  have h1 : ((1 / 2) ^ n * (2 : ℂ) ^ n) = 1:= by
-    rw [← IsUnit.eq_mul_inv_iff_mul_eq]
-    · simp
-    · simp
-  rw [h1]
-  simp only [mul_one, one_mul, c]
-  have h1 : Complex.ofReal |(√(Q.m * (Q.ω * Q.ℏ⁻¹)))⁻¹| = (√(Q.m * (Q.ω * Q.ℏ⁻¹)))⁻¹ := by
-    congr
-    apply abs_of_nonneg
-    refine inv_nonneg_of_nonneg ?_
-    exact Real.sqrt_nonneg (Q.m * (Q.ω * Q.ℏ⁻¹))
-  rw [h1]
-  have h1 : √(Q.m * (Q.ω * (Real.pi⁻¹ * Q.ℏ⁻¹))) = (√(Q.m * (Q.ω * Q.ℏ⁻¹))) * (√(Real.pi⁻¹)) := by
-    trans √((Q.m * (Q.ω * Q.ℏ⁻¹)) * Real.pi⁻¹)
+  have h1 : √(Q.m * Q.ω * Real.pi⁻¹ * Q.ℏ⁻¹) = Q.ξ⁻¹* (√(Real.pi⁻¹)) := by
+    trans √((Q.m * Q.ω * Q.ℏ⁻¹) * Real.pi⁻¹)
     · ring_nf
-    refine Real.sqrt_mul' (Q.m * (Q.ω * Q.ℏ⁻¹)) ?_
-    refine inv_nonneg_of_nonneg ?_
-    exact Real.pi_nonneg
-  rw [h1]
-  simp only [Real.sqrt_inv, mul_comm, Complex.ofReal_mul, Complex.ofReal_inv, c]
-  ring_nf
-  have h1 : ↑√Real.pi * (↑√Real.pi : ℂ)⁻¹ =1 := by
-    rw [← IsUnit.eq_mul_inv_iff_mul_eq]
-    simp only [inv_inv, one_mul, c]
-    simp only [isUnit_iff_ne_zero, ne_eq, inv_eq_zero, Complex.ofReal_eq_zero, c]
-    refine Real.sqrt_ne_zero'.mpr ?_
-    exact Real.pi_pos
+    rw [Real.sqrt_mul' _ (inv_nonneg_of_nonneg Real.pi_nonneg), ξ_inverse]
+    field_simp
   rw [h1]
-  simp only [one_mul, c]
-  suffices h2 : IsUnit (↑√(Q.m * Q.ω * Q.ℏ⁻¹) : ℂ) by
-    rw [mul_comm, ← IsUnit.eq_mul_inv_iff_mul_eq h2]
-    simp only [one_mul, c]
-  simp only [isUnit_iff_ne_zero, ne_eq, Complex.ofReal_eq_zero, c]
-  refine Real.sqrt_ne_zero'.mpr ?_
-  rw [propext (lt_mul_inv_iff₀ Q.hℏ)]
-  simp only [zero_mul, c]
-  exact mul_pos Q.hm Q.hω
+  have : (n ! : ℂ) ≠ 0 := Complex.ne_zero_of_re_pos <| by simpa using factorial_pos n
+  have := Complex.ofReal_ne_zero.mpr (ne_of_gt Q.ξ_pos)
+  have := Complex.ofReal_ne_zero.mpr (Real.sqrt_ne_zero'.mpr Real.pi_pos)
+  field_simp
 
 /-- The eigen-functions of the quantum harmonic oscillator are orthogonal. -/
 lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
@@ -374,29 +304,18 @@ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
   conv_lhs =>
     enter [2, x]
     rw [eigenfunction_conj, Q.eigenfunction_mul n p]
-  rw [MeasureTheory.integral_mul_left]
-  rw [integral_complex_ofReal]
-  let c := √(Q.m * Q.ω / Q.ℏ)
-  have h1 : c ^ 2 = Q.m * Q.ω / Q.ℏ := by
-    trans c * c
-    · exact pow_two c
-    simp only [c]
-    refine Real.mul_self_sqrt ?_
-    refine div_nonneg ?_ ?_
-    exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
-    exact le_of_lt Q.hℏ
-  have hc : (∫ (x : ℝ), (physHermite n (c * x) * physHermite p (c * x)) *
-      Real.exp (-Q.m * Q.ω * x ^ 2 / Q.ℏ))
-      = ∫ (x : ℝ), (physHermite n (c * x) * physHermite p (c * x)) *
-      Real.exp (- c^2 * x ^ 2) := by
+  rw [MeasureTheory.integral_mul_left, integral_complex_ofReal]
+  have hc : (∫ (x : ℝ), (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) *
+      physHermite p (√(Q.m * Q.ω / Q.ℏ) * x)) *  Real.exp (-Q.m * Q.ω * x ^ 2 / Q.ℏ))
+      = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) * physHermite p (1/Q.ξ * x)) *
+      Real.exp (- (1/Q.ξ)^2 * x ^ 2) := by
     congr
     funext x
-    congr
-    simp only [neg_mul, h1, c]
-    field_simp
+    rw [one_over_ξ_sq]
+    field_simp [neg_mul, one_over_ξ, one_over_ξ_sq]
   rw [hc, physHermite_orthogonal_cons hnp]
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
-      mul_one, Complex.ofReal_zero, mul_zero, c]
+    mul_one, Complex.ofReal_zero, mul_zero]
 
 /-- The eigenfunctions are orthonormal within the Hilbert space. -/
 lemma eigenfunction_orthonormal :
@@ -409,6 +328,11 @@ lemma eigenfunction_orthonormal :
   · simp only [hnp, reduceIte]
     exact Q.eigenfunction_orthogonal hnp
 
+/-- The eigenfunctions are linearly independent. -/
+lemma eigenfunction_linearIndependent :
+    LinearIndependent ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) :=
+  Q.eigenfunction_orthonormal.linearIndependent
+
 end HarmonicOscillator
 end OneDimension
 end QuantumMechanics