diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
index 2d049d65..7e00f5ac 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
@@ -7,6 +7,7 @@ import PhysLean.Mathematics.SpecialFunctions.PhyscisistsHermite
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Parity
+import PhysLean.Meta.TODO.Basic
 /-!
 
 # 1d Harmonic Oscillator
@@ -72,7 +73,8 @@ structure HarmonicOscillator where
 namespace HarmonicOscillator
 
 open Nat
-open PhysLean
+open PhysLean HilbertSpace
+open MeasureTheory
 
 variable (Q : HarmonicOscillator)
 
@@ -96,12 +98,19 @@ lemma ℏ_ne_zero : Q.ℏ ≠ 0 := by
   have h1 := Q.hℏ
   linarith
 
-/-- The characteristic length of the harmonic oscilator.
-  Defined as `√(ℏ /(m ω))`. -/
+/-!
+
+## The characteristic length
+
+-/
+
+/-- The characteristic length `ξ` of the harmonic oscilator is defined
+  as `√(ℏ /(m ω))`. -/
 noncomputable def ξ : ℝ := √(Q.ℏ / (Q.m * Q.ω))
 
 lemma ξ_nonneg : 0 ≤ Q.ξ := Real.sqrt_nonneg _
 
+@[simp]
 lemma ξ_pos : 0 < Q.ξ := by
   rw [ξ]
   apply Real.sqrt_pos.mpr
@@ -109,6 +118,16 @@ lemma ξ_pos : 0 < Q.ξ := by
   · exact Q.hℏ
   · exact mul_pos Q.hm Q.hω
 
+@[simp]
+lemma ξ_ne_zero : Q.ξ ≠ 0 := Ne.symm (_root_.ne_of_lt Q.ξ_pos)
+
+lemma ξ_sq : Q.ξ^2 = Q.ℏ / (Q.m * Q.ω) := by
+  rw [ξ]
+  apply Real.sq_sqrt
+  apply div_nonneg
+  · exact le_of_lt Q.hℏ
+  · exact mul_nonneg (le_of_lt Q.hm) (le_of_lt Q.hω)
+
 @[simp]
 lemma ξ_abs : abs Q.ξ = Q.ξ := abs_of_nonneg Q.ξ_nonneg
 
@@ -124,6 +143,28 @@ 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)
 
+TODO "The momentum operator should be moved to a more general file."
+
+/-- The momentum operator is defined as the map from `ℝ → ℂ` to `ℝ → ℂ` taking
+  `ψ` to `- i ℏ ψ'`.
+
+  The notation `Pᵒᵖ` can be used for the momentum operator. -/
+noncomputable def momentumOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
+  fun x => - Complex.I * Q.ℏ * deriv ψ x
+
+@[inherit_doc momentumOperator]
+scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Pᵒᵖ" => momentumOperator
+
+/-- The position operator is defined as the map from `ℝ → ℂ` to `ℝ → ℂ` taking
+  `ψ` to `x ψ'`.
+
+  The notation `Xᵒᵖ` can be used for the momentum operator. -/
+noncomputable def positionOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
+  fun x => x * ψ x
+
+@[inherit_doc positionOperator]
+scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Xᵒᵖ" => positionOperator
+
 /-- For a harmonic oscillator, the Schrodinger Operator corresponding to it
   is defined as the function from `ℝ → ℂ` to `ℝ → ℂ` taking
 
@@ -131,7 +172,24 @@ lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / Q.ℏ := by
 noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ :=
   fun x => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) x) + 1/2 * Q.m * Q.ω^2 * x^2 * ψ x
 
-open HilbertSpace
+lemma schrodingerOperator_eq (ψ : ℝ → ℂ) :
+    Q.schrodingerOperator ψ = (- Q.ℏ ^ 2 / (2 * Q.m)) •
+    (deriv (deriv ψ)) + (1/2 * Q.m * Q.ω^2) • ((fun x => Complex.ofReal x ^2) * ψ) := by
+  funext x
+  simp only [schrodingerOperator, one_div, Pi.add_apply, Pi.smul_apply, Complex.real_smul,
+    Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow, Complex.ofReal_mul,
+    Complex.ofReal_ofNat, Pi.mul_apply, Complex.ofReal_inv, add_right_inj]
+  ring
+
+/-- The schrodinger operator written in terms of `ξ`. -/
+lemma schrodingerOperator_eq_ξ (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ =
+    fun x => (Q.ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) +  (1/Q.ξ^2 )^2 * x^2 * ψ x) := by
+  funext x
+  simp [schrodingerOperator_eq, ξ_sq, ξ_inverse, ξ_ne_zero, ξ_pos, ξ_abs, ← Complex.ofReal_pow]
+  have hm' := Complex.ofReal_ne_zero.mpr Q.m_ne_zero
+  have hℏ' := Complex.ofReal_ne_zero.mpr Q.ℏ_ne_zero
+  field_simp
+  ring
 
 /-- The Schrodinger operator commutes with the parity operator. -/
 lemma schrodingerOperator_parity (ψ : ℝ → ℂ) :
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
index 5b10c18f..cbc747bd 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
@@ -53,11 +53,11 @@ lemma mul_eigenfunction_integrable (f : ℝ → ℂ) (hf : MemHS f) :
     simp
 
 lemma mul_physHermite_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
-    MeasureTheory.Integrable (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
-      (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
-  have h2 : (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) • (fun (x : ℝ) =>
-      (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) *
-      (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) = fun x =>
+    MeasureTheory.Integrable (fun x => physHermite n (x/Q.ξ) *
+      (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ^2))))) := by
+  have h2 : (1 / ↑√(2 ^ n * ↑n !) * (1/ √(√Real.pi * Q.ξ)) : ℂ) • (fun (x : ℝ) =>
+      (physHermite n (x / Q.ξ) *
+      (f x * Real.exp (- x ^ 2 / (2 * Q.ξ^2))))) = fun x =>
       Q.eigenfunction n x * f x := by
     funext x
     simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
@@ -74,21 +74,19 @@ lemma mul_physHermite_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
     Real.sqrt_nonneg, not_or]
   apply And.intro
   · exact factorial_ne_zero n
-  · apply Real.sqrt_ne_zero'.mpr
-    refine div_pos ?_ ?_
-    · exact mul_pos Q.hm Q.hω
-    · apply mul_pos Real.pi_pos Q.hℏ
+  · apply And.intro
+    · exact Real.sqrt_ne_zero'.mpr Q.ξ_pos
+    · exact Real.sqrt_ne_zero'.mpr Real.pi_pos
 
 lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial ℤ) :
-    MeasureTheory.Integrable (fun x => (P (√(Q.m * Q.ω / Q.ℏ) * x)) *
-      (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by
+    MeasureTheory.Integrable (fun x => (P (x /Q.ξ)) *
+      (f x * Real.exp (- x^2 / (2 * Q.ξ^2)))) volume := by
   have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑(P (√(Q.m * Q.ω / Q.ℏ) * x)) *
-    (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(Q.m * Q.ω / Q.ℏ) * x)) *
-    (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by
+  have h2 : (fun x => ↑(P (x/Q.ξ)) * (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ^2)))))
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (x/Q.ξ)) *
+    (f x * Real.exp (- x ^ 2 / (2 * Q.ξ^2)))) := by
     funext x
     rw [← ha]
     rw [← Finset.sum_mul]
@@ -99,48 +97,36 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
   apply MeasureTheory.integrable_finset_sum
   intro i hi
   simp only [mul_assoc]
-  have hf' : (fun a_1 =>
-    ↑(a i) * (↑(physHermite i (√(Q.m * Q.ω / Q.ℏ) * a_1)) *
-    (f a_1 * ↑(Real.exp (- Q.m * (Q.ω * a_1 ^ 2) / (2 * Q.ℏ))))))
-    = fun x => (a i) • ((physHermite i (√(Q.m * Q.ω / Q.ℏ) * x)) *
-      (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
+  have hf' : (fun x => ↑(a i) * (physHermite i (x/Q.ξ) *
+    (f x * Real.exp (- (x ^ 2) / (2 * Q.ξ^2)))))
+    = fun x => (a i) • (physHermite i (x/Q.ξ) * (f x * Real.exp (- x ^ 2 / (2 * Q.ξ^2)))) := by
     funext x
     simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
       Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, Complex.real_smul,
       mul_eq_mul_left_iff, Complex.ofReal_eq_zero]
-    ring_nf
-    simp_all
   rw [hf']
   apply MeasureTheory.Integrable.smul
   exact Q.mul_physHermite_integrable f hf i
 
 lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
-    MeasureTheory.Integrable (fun x => x ^ r *
-      (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by
+    MeasureTheory.Integrable (fun x => x ^ r * (f x * Real.exp (- x^2 / (2 * Q.ξ^2)))) volume := by
   by_cases hr : r ≠ 0
   · have h1 := Q.mul_polynomial_integrable f hf (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 => (↑√(Q.m * Q.ω / Q.ℏ) * ↑x) ^ r *
-      (f x * Complex.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))))
-      = (↑√(Q.m * Q.ω / Q.ℏ) : ℂ) ^ r • (fun x => (↑x ^r *
-      (f x * Real.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))))) := by
+    have h2 : (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))))) := by
       funext x
       simp only [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 [h2] at h1
-    suffices h2 : IsUnit (↑(√(Q.m * Q.ω / Q.ℏ) ^ r : ℂ)) by
+    suffices h2 : IsUnit (↑((1/Q.ξ)^ r : ℂ)) by
       rw [IsUnit.integrable_smul_iff h2] at h1
       simpa using h1
     simp only [isUnit_iff_ne_zero, ne_eq, pow_eq_zero_iff', Complex.ofReal_eq_zero, not_and,
       Decidable.not_not]
-    have h1 : √(Q.m * Q.ω / Q.ℏ) ≠ 0 := by
-      refine Real.sqrt_ne_zero'.mpr ?_
-      refine div_pos ?_ ?_
-      · exact mul_pos Q.hm Q.hω
-      · exact Q.hℏ
-    simp [h1]
+    simp
   · simp only [ne_eq, Decidable.not_not] at hr
     subst hr
     simpa using Q.mul_physHermite_integrable f hf 0
@@ -167,14 +153,13 @@ 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)) *
-    (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
+    (n : ℕ) : ∫ (x : ℝ), (physHermite n (x / Q.ξ)) * (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ ^ 2))))
     = 0 := by
   have h1 := Q.orthogonal_eigenfunction_of_mem_orthogonal f hf hOrth n
   have h2 : (fun (x : ℝ) =>
-          (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) *
-            (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) * f x *
-            Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
+          (1 / ↑√(2 ^ n * ↑n !) * (1/ √(√Real.pi * Q.ξ)) : ℂ) *
+            (physHermite n (x/Q.ξ) * f x *
+            Real.exp (- x ^ 2 / (2 * Q.ξ^2))))
     = fun x => Q.eigenfunction n x * f x := by
     funext x
     simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
@@ -190,12 +175,8 @@ lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     or_false, Real.sqrt_nonneg] at h1
   have h0 : n ! ≠ 0 := by
     exact factorial_ne_zero n
-  have h0' : √(Q.m * Q.ω / (Real.pi * Q.ℏ)) ≠ 0 := by
-    simp only [ne_eq]
-    refine Real.sqrt_ne_zero'.mpr ?_
-    refine div_pos ?_ ?_
-    · exact mul_pos hm hω
-    · apply mul_pos Real.pi_pos hℏ
+  have h0' : ¬ (√Q.ξ = 0 ∨ √Real.pi = 0):= by
+    simpa using And.intro (Real.sqrt_ne_zero'.mpr Q.ξ_pos) (Real.sqrt_ne_zero'.mpr Real.pi_pos)
   simp only [h0, h0', or_self, false_or] at h1
   rw [← h1]
   congr
@@ -207,14 +188,14 @@ 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 (x /Q.ξ)) * (f x * Real.exp (- x^2 / (2 * Q.ξ^2))) = 0 := by
   have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑(P (√(m * ω / ℏ) * x)) *
-    (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(m * ω / ℏ) * x)) *
-    (f x * Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) := by
+  have h2 : (fun x => ↑(P (x /Q.ξ)) *
+    (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ^2)))))
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (x/Q.ξ)) *
+    (f x * Real.exp (- x ^ 2 / (2 * Q.ξ^2)))) := by
     funext x
     rw [← ha]
     rw [← Finset.sum_mul]
@@ -233,19 +214,14 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth x]
     congr
     funext x
-    simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
-      Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, mul_eq_mul_left_iff,
-      Complex.ofReal_eq_zero]
-    left
-    left
-    congr 1
-    ring
+    simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
+      Complex.ofReal_mul, Complex.ofReal_ofNat]
   · /- Integrablility -/
     intro i hi
-    have hf' : (fun x => ↑(a i) * ↑(physHermite i (√(m * ω / ℏ) * x)) *
-        (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-        = a i • (fun x => (physHermite i (√(m * ω / ℏ) * x)) *
-        (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) := by
+    have hf' : (fun x => ↑(a i) * ↑(physHermite i (x /Q.ξ)) *
+        (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ^2)))))
+        = a i • (fun x => (physHermite i (x/Q.ξ)) *
+        (f x * ↑(Real.exp (- x ^ 2 / (2 * Q.ξ^2))))) := by
       funext x
       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,
@@ -258,35 +234,26 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
 /-- 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 ℏ))`
+  `x ^ r * e ^ (- x ^ 2 / (2 ξ^2))`
 
   the proof of this result relies on the fact that Hermite polynomials span polynomials. -/
 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
+    (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 => (↑√(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
+    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 [_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
+    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
@@ -305,7 +272,7 @@ open Finset
 /-- 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 ℏ))`
+  `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)`
@@ -314,23 +281,23 @@ open Finset
 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
+    (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 (- m * ω * y^2 / (2 * ℏ))))
+        (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 (- m * ω * y^2 / (2 * ℏ))))) := by
+      (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 (- m * ω * y^2 / (2 * ℏ)))) =
+        * (f y * Real.exp (- y^2 / (2 * Q.ξ^2)))) =
         fun n => (∑ r ∈ range n,
         (Complex.I * ↑c * ↑y) ^ r / r !)
-        * ((f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) := by
+        * ((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 (- m * ω * y^2 / (2 * ℏ))))
-      = (Complex.exp (Complex.I * c * y)) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))) := by
+    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
@@ -341,19 +308,19 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
   /- 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 * ℏ))))
+      (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 (- m * ω * y^2 / (2 * ℏ))))) := by
+      (f y * Real.exp (- y^2 / (2 * Q.ξ^2))))) := by
     let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * Complex.abs (f x) *
-      (Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))
+      (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 (-m * ω * a ^ 2 / (2 * ℏ)))))
+        (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
         = fun a => (Complex.I * ↑c) ^ r / ↑r ! *
-        (f a * Complex.ofReal (a ^ r * (Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by
+        (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]
@@ -364,10 +331,10 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       · 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 * ℏ)))) =
+        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 (- (m * ω / (2* ℏ)) * x ^ 2))) := by
+            (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]
@@ -378,7 +345,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
         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
+          Real.exp (-(1/ (2 * Q.ξ^2)) * x ^ 2)) := by
         simp only [neg_mul, bound]
         funext x
         congr
@@ -386,10 +353,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       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
+      · simp
     · intro n
       apply Filter.Eventually.of_forall
       intro y
@@ -400,13 +364,13 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       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
+      have h1 : (Complex.abs (f y) * Complex.abs (Complex.exp (-(↑y ^ 2) / (2 * Q.ξ^2))))
+        = Complex.abs (f y) * Real.exp (-(y ^ 2) / (2 * Q.ξ^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
+        trans (Complex.ofReal (- y ^ 2 / (2 * Q.ξ^2))).re
         · congr
           simp
         · rw [Complex.ofReal_re]
@@ -430,21 +394,21 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       · 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 * ℏ))
+        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 (- m * ω * y^2 / (2 * ℏ)))) = fun (n : ℕ) => 0 := by
+      (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 (-m * ω * a ^ 2 / (2 * ℏ)))))
+        (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
         = fun a => ((Complex.I * ↑c) ^ r / ↑r !) *
-        (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by
+        (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]
@@ -455,9 +419,9 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       simp
     · intro r hr
       have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! *
-        (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ)))))
+        (f a * ↑(Real.exp (- a ^ 2 / (2 * Q.ξ^2)))))
         = ((Complex.I * ↑c) ^ r / ↑r !) •
-        fun a => (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by
+        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]
@@ -475,14 +439,14 @@ open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology
 /-- 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 ℏ))`
+  `f (x) * e ^ (- x ^ 2 / (2 ξ^2))`
 
   is zero.
 
   The proof of this result relies on `orthogonal_exp_of_mem_orthogonal`. -/
 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
+    𝓕 (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,
@@ -492,8 +456,8 @@ lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
   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 * ↑ℏ))) = _
+  change Complex.exp (-(2 * ↑Real.pi * (x * c) * Complex.I)) *
+    (f x * Complex.exp (- x ^ 2 / (2 * Q.ξ^2))) = _
   congr 2
   ring
 
@@ -502,33 +466,27 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f)
     (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2),
       eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) :
     HilbertSpace.mk hf = 0 := by
-  have hf' : (fun x => f x * ↑(rexp (-m * ω * x ^ 2 / (2 * ℏ))))
-        = (fun x => f x * ↑(rexp (- (m * ω / (2 * ℏ)) * (x - 0) ^ 2))) := by
+  have hf' : (fun x => f x * ↑(rexp (- x ^ 2 / (2 * Q.ξ^2))))
+        = (fun x => f x * ↑(rexp (- (1/ (2 * Q.ξ^2)) * (x - 0) ^ 2))) := by
     funext x
     simp only [neg_mul, ofReal_exp, ofReal_div, ofReal_neg, ofReal_mul, ofReal_pow,
       ofReal_ofNat, sub_zero, mul_eq_mul_left_iff]
     left
     congr
     field_simp
-  have h1 : eLpNorm (fun x => f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) 2 volume = 0 := by
+  have h1 : eLpNorm (fun x => f x * Real.exp (- x^2 / (2 * Q.ξ^2))) 2 volume = 0 := by
     rw [← plancherel_theorem]
     rw [Q.fourierIntegral_zero_of_mem_orthogonal f hf hOrth]
     simp only [eLpNorm_zero]
-    · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is integrable -/
+    · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is integrable -/
       rw [hf']
       rw [← memℒp_one_iff_integrable]
-      apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (m * ω / (2 * ℏ)) 0
-      refine div_pos ?_ ?_
-      · exact mul_pos hm hω
-      · have h1 := Q.hℏ
-        linarith
-    · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is square-integrable -/
+      apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (1/ (2 * Q.ξ^2)) 0
+      simp
+    · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is square-integrable -/
       rw [hf']
-      refine HilbertSpace.mul_gaussian_mem_Lp_two f hf (m * ω / (2 * ℏ)) 0 ?_
-      refine div_pos ?_ ?_
-      · exact mul_pos hm hω
-      · have h1 := Q.hℏ
-        linarith
+      refine HilbertSpace.mul_gaussian_mem_Lp_two f hf (1 / (2 * Q.ξ^2)) 0 ?_
+      simp
   refine (norm_eq_zero_iff (by simp)).mp ?_
   simp only [Norm.norm, eLpNorm_mk]
   have h2 : eLpNorm f 2 volume = 0 := by
@@ -539,15 +497,12 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f)
     exact h1
     exact aeStronglyMeasurable_of_memHS hf
     simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true]
-    · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is strongly measurable -/
+    · /- f x * Real.exp (- x^2 / (2 * ξ^2)) is strongly measurable -/
       rw [hf']
       apply Integrable.aestronglyMeasurable
       rw [← memℒp_one_iff_integrable]
-      apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (m * ω / (2 * ℏ)) 0
-      refine div_pos ?_ ?_
-      · exact mul_pos hm hω
-      · have h1 := Q.hℏ
-        linarith
+      apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (1/ (2 * Q.ξ^2)) 0
+      simp
     · simp
   rw [h2]
   simp
@@ -567,7 +522,7 @@ lemma zero_of_orthogonal_eigenVector (f : HilbertSpace)
   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 * ℏ)`
+  `f x * e ^ (- x^2 / (2 * ξ^2))`
 
   is zero for `f` orthogonal to all eigenfunctions, and hence the norm of `f` is zero.
 -/
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
index 3ed29c6d..9f592893 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
@@ -21,21 +21,21 @@ variable (Q : HarmonicOscillator)
 open Nat
 open PhysLean
 open HilbertSpace
+open MeasureTheory
 
 /-- 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ℏ)`.
+  `1/√(2^n n!) 1/√(√π ξ) * physHermite n (x / ξ) * e ^ (- x²/ (2 ξ²))`.
 
 -/
 noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun 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.ℏ))
+  1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ)) * physHermite n (x / Q.ξ) *
+  Real.exp (- x^2 / (2 * Q.ξ^2))
 
 lemma eigenfunction_eq (n : ℕ) :
-    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
+    Q.eigenfunction n = fun (x : ℝ) => (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) *
+    Complex.ofReal (physHermite n (x / Q.ξ) * Real.exp (- x^2 / (2 * Q.ξ^2))) := by
   funext x
   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,
@@ -43,20 +43,19 @@ lemma eigenfunction_eq (n : ℕ) :
   ring
 
 lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) =>
-    √√(Q.m * Q.ω / (Real.pi * Q.ℏ)) * Complex.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) := by
+    (1/ √(√Real.pi * Q.ξ)) * Complex.exp (- x^2 / (2 * Q.ξ^2)):= by
   funext x
   simp [eigenfunction]
 
 lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
     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
+    * Complex.ofReal (physHermite n (x / Q.ξ)) * Q.eigenfunction 0 x := by
   match n with
   | 0 =>
     simp
   | n + 1 =>
     funext x
     field_simp [eigenfunction, eigenfunction_zero]
-    ring
 
 /-!
 
@@ -66,21 +65,15 @@ lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
 
 /-- The eigenfunctions are integrable. -/
 @[fun_prop]
-lemma eigenfunction_integrable (n : ℕ) : MeasureTheory.Integrable (Q.eigenfunction n) := by
+lemma eigenfunction_integrable (n : ℕ) : 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
+  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
-    simp only [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp]
-    left
-    field_simp
+    ring_nf
   rw [h1]
   apply guassian_integrable_polynomial_cons
   simp
@@ -93,14 +86,14 @@ lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
   simp [-Complex.ofReal_exp]
 
 lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
-    ‖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
+    ‖Q.eigenfunction n x‖ = (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) *
+    (|physHermite n (x / Q.ξ)| * Real.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) := by
   rw [eigenfunction_eq]
   simp only [neg_mul, Complex.ofReal_mul, Complex.norm_eq_abs]
   rw [AbsoluteValue.map_mul, AbsoluteValue.map_mul]
   congr
   · simp [Real.sqrt_nonneg, abs_of_nonneg]
-  · simp
+  · simp [Real.sqrt_nonneg, abs_of_nonneg]
   · rw [AbsoluteValue.map_mul]
     congr 1
     · simp
@@ -108,11 +101,10 @@ lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
       simp [abs_of_nonneg]
 
 lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) :
-    ‖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 : ℝ))
+    ‖Q.eigenfunction n x‖ ^ 2 = (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) ^ 2 *
+    ((physHermite n (x / Q.ξ)) ^ 2 * Real.exp (- x^2 / Q.ξ ^ 2)) := by
+  trans (1/√(2 ^ n * n !) * (1/ √(√Real.pi * Q.ξ))) ^ 2 *
+    (|physHermite n (x/Q.ξ)| ^ 2 * Real.exp (- x^2 / (2 * Q.ξ ^2)) ^ (2 : ℝ))
   · simp only [Real.rpow_two]
     rw [eigenfunction_point_norm]
     ring
@@ -126,14 +118,16 @@ lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) :
 @[fun_prop]
 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
+  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
@@ -172,6 +166,7 @@ lemma eigenfunction_parity (n : ℕ) :
   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
@@ -185,28 +180,25 @@ 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/√(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
+    1/√(2 ^ n * n !) * 1/√(2 ^ p * p !) * (1/ (√Real.pi * Q.ξ)) * Complex.ofReal
+    (physHermite n (x / Q.ξ) * physHermite p (x / Q.ξ) * Real.exp (- x^2 / Q.ξ^2)) := by
   calc Q.eigenfunction n x * Q.eigenfunction p x
-    _ = (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
+    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * ((1/ ((√(√Real.pi * Q.ξ)) * √(√Real.pi * Q.ξ)))) *
+        (physHermite n (x/Q.ξ) * physHermite p (x/Q.ξ)) *
+        (Real.exp (- x^2 / (2 * Q.ξ^2)) * Real.exp (- x^2 / (2 * Q.ξ^2))) := 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 !) * 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
+    _ = (1/√(2 ^ n * n !) * 1/√(2 ^ p * p !)) * (1/ (√Real.pi * Q.ξ))  *
+        (physHermite n (x / Q.ξ) *  physHermite p (x / Q.ξ)) * (Real.exp (- x^2 / Q.ξ^2)) := by
       congr 1
       · congr 1
         · congr 1
-          · rw [← Complex.ofReal_mul]
-            congr
-            refine Real.mul_self_sqrt ?_
-            exact Real.sqrt_nonneg (Q.m * Q.ω / (Real.pi * Q.ℏ))
+          · congr 1
+            rw [← Complex.ofReal_mul, Real.mul_self_sqrt]
+            · simp
+            · simp
       · rw [← Complex.ofReal_mul]
         congr
         rw [← Real.exp_add]
@@ -219,46 +211,22 @@ lemma eigenfunction_mul (n p : ℕ) :
   ring
 
 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/√(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 !)) * √(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
-          · trans 1 / ↑(√(2 ^ n * ↑n !) * ↑√(2 ^ n * ↑n !))
-            · field_simp
-            congr
-            trans Complex.ofReal ((2 ^ n * ↑n !))
-            · congr 1
-              refine Real.mul_self_sqrt ?_
-              refine Left.mul_nonneg ?_ (cast_nonneg' n !)
-              refine pow_nonneg ?_ n
-              simp only [ofNat_nonneg]
-            simp
-          · rw [← Complex.ofReal_mul]
-            congr
-            refine Real.mul_self_sqrt ?_
-            exact Real.sqrt_nonneg (Q.m * Q.ω / (Real.pi * Q.ℏ))
-      · rw [← Complex.ofReal_mul]
-        congr
-        rw [← Real.exp_add]
-        simp only [neg_mul, Real.exp_eq_exp]
-        field_simp
-        ring
-  simp only [one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div,
-    Complex.ofReal_neg, Complex.ofReal_mul, Complex.ofReal_pow]
-  ring
+    (1/ (2 ^ n * n !) * (1/ (√Real.pi * Q.ξ))) *
+    Complex.ofReal ((physHermite n (x / Q.ξ))^2 * Real.exp (- x^2 / Q.ξ^2)) := by
+  rw [eigenfunction_mul]
+  congr 2
+  · trans 1 / ↑(√(2 ^ n * ↑n !) * ↑√(2 ^ n * ↑n !))
+    · field_simp
+    congr
+    trans Complex.ofReal ((2 ^ n * ↑n !))
+    · congr 1
+      refine Real.mul_self_sqrt ?_
+      refine Left.mul_nonneg ?_ (cast_nonneg' n !)
+      refine pow_nonneg ?_ n
+      simp only [ofNat_nonneg]
+    · simp
+  · congr 1
+    exact (pow_two ((fun x => (Polynomial.aeval x) (physHermite n)) (x / Q.ξ))).symm
 
 open InnerProductSpace
 
@@ -270,31 +238,19 @@ lemma eigenfunction_normalized (n : ℕ) : ⟪HilbertSpace.mk (Q.eigenfunction_m
     enter [2, x]
     rw [eigenfunction_conj, Q.eigenfunction_mul_self]
   rw [MeasureTheory.integral_mul_left, integral_complex_ofReal]
-  have hc : (∫ (x : ℝ), physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 *
-      Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ))
+  have hc : (∫ (x : ℝ), physHermite n (x /Q.ξ) ^ 2 * Real.exp (- x ^ 2 / Q.ξ^2))
       = ∫ (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 [one_over_ξ]
-      exact pow_two _
-    · simp only [neg_mul, one_over_ξ_sq]
-      field_simp
+    ring_nf
   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]
-  ring_nf
-  have h1 : √(Q.m * Q.ω * Real.pi⁻¹ * Q.ℏ⁻¹) = Q.ξ⁻¹* (√(Real.pi⁻¹)) := by
-    trans √((Q.m * Q.ω * Q.ℏ⁻¹) * Real.pi⁻¹)
-    · ring_nf
-    rw [Real.sqrt_mul' _ (inv_nonneg_of_nonneg Real.pi_nonneg), ξ_inverse]
-    field_simp
-  rw [h1]
+  simp only [one_div, mul_inv_rev, inv_inv, ξ_abs]
   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
+  ring
 
 /-- The eigen-functions of the quantum harmonic oscillator are orthogonal. -/
 lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
@@ -305,14 +261,12 @@ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
     enter [2, x]
     rw [eigenfunction_conj, Q.eigenfunction_mul n p]
   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.ℏ))
+  have hc : (∫ (x : ℝ), (physHermite n (x/Q.ξ) * physHermite p (x/Q.ξ)) * Real.exp (-x ^ 2 / Q.ξ^2))
       = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) * physHermite p (1/Q.ξ * x)) *
       Real.exp (- (1/Q.ξ)^2 * x ^ 2) := by
     congr
     funext x
-    rw [one_over_ξ_sq]
-    field_simp [neg_mul, one_over_ξ, one_over_ξ_sq]
+    ring_nf
   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]
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
index b238d16b..9b53d2cb 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
@@ -24,15 +24,21 @@ open HilbertSpace
 /-- The `n`th eigenvalues for a Harmonic oscillator is defined as `(n + 1/2) * ℏ * ω`. -/
 noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω
 
+/-!
+
+## Derivatives of the eigenfunctions
+
+-/
+
 lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) =
-    Complex.ofReal (- Q.m * Q.ω / Q.ℏ) • Complex.ofReal * Q.eigenfunction 0 := by
+    Complex.ofReal (- 1 / Q.ξ ^2) • Complex.ofReal * Q.eigenfunction 0 := by
   rw [eigenfunction_zero]
   simp only [neg_mul, deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_neg,
     Complex.ofReal_mul, Algebra.smul_mul_assoc]
   ext x
-  have h1 : deriv (fun x => Complex.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))) x =
-      - Q.m * Q.ω * x /Q.ℏ* Complex.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ)) := by
-    trans deriv (Complex.exp ∘ (fun x => -(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))) x
+  have h1 : deriv (fun (x : ℝ) => Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) x =
+      - x /Q.ξ^2 * Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2)) := by
+    trans deriv (Complex.exp ∘ (fun (x : ℝ) => - x ^ 2 / (2 * Q.ξ ^ 2))) x
     · rfl
     rw [deriv_comp]
     simp only [Complex.deriv_exp, deriv_div_const, deriv.neg', differentiableAt_const,
@@ -47,58 +53,46 @@ lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) =
       rw [deriv_mul]
       simp only [Complex.deriv_ofReal, one_mul, mul_one]
       ring
-      exact Complex.differentiableAt_ofReal
-      exact Complex.differentiableAt_ofReal
+      · exact Complex.differentiableAt_ofReal
+      · exact Complex.differentiableAt_ofReal
     rw [h1']
     field_simp
     ring
     exact Complex.differentiableAt_exp
     refine DifferentiableAt.mul_const ?_ _
     refine differentiableAt_neg_iff.mpr ?_
-    refine DifferentiableAt.const_mul ?_ _
     refine DifferentiableAt.pow ?_ 2
     exact Complex.differentiableAt_ofReal
   simp only [Pi.smul_apply, Pi.mul_apply, smul_eq_mul]
   rw [h1]
+  simp only [Real.sqrt_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
+    Complex.ofReal_one, Complex.ofReal_pow]
   ring
 
-lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0)) x =
-    - (Q.m * Q.ω) / Q.ℏ * (Q.eigenfunction 0 x +
-    x * (-(Q.m * Q.ω) / Q.ℏ * x * Q.eigenfunction 0 x)) := by
-  simp only [deriv_eigenfunction_zero, neg_mul, Complex.ofReal_div, Complex.ofReal_neg,
-    Complex.ofReal_mul, Algebra.smul_mul_assoc]
-  trans deriv (fun x => (-(↑Q.m * ↑Q.ω) / ↑Q.ℏ) • (Complex.ofReal x * Q.eigenfunction 0 x)) x
-  · congr
-    funext x
-    simp
-  simp only [Complex.real_smul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul,
-    differentiableAt_const, deriv_const_mul_field', mul_eq_mul_left_iff, div_eq_zero_iff,
-    neg_eq_zero, _root_.mul_eq_zero, Complex.ofReal_eq_zero]
-  rw [deriv_mul (by fun_prop) (by fun_prop)]
-  simp only [differentiableAt_const, deriv_const_mul_field', Complex.deriv_ofReal, mul_one]
+lemma deriv_eigenfunction_zero' : deriv (Q.eigenfunction 0) =
+    (- √2  / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := by
   rw [deriv_eigenfunction_zero]
-  simp only [neg_mul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul, Pi.mul_apply,
-    Pi.smul_apply, smul_eq_mul]
+  funext x
+  simp only [Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_pow,
+    eigenfunction_eq, pow_zero, factorial_zero, cast_one, mul_one, Real.sqrt_one, ne_eq,
+    one_ne_zero, not_false_eq_true, div_self, Real.sqrt_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
+    one_div, mul_inv_rev, one_mul, Polynomial.aeval, physHermite_zero, eq_intCast, Int.cast_one,
+    Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_one, Complex.ofReal_exp, Complex.ofReal_ofNat,
+    Pi.mul_apply, Pi.smul_apply, smul_eq_mul, pow_one, factorial_one, physHermite_one,
+    Polynomial.eval₂_mul, Polynomial.eval₂_ofNat, Polynomial.eval₂_X]
   ring_nf
-  left
-  trivial
-
-lemma schrodingerOperator_eigenfunction_zero (x : ℝ) :
-    Q.schrodingerOperator (Q.eigenfunction 0) x = Q.eigenValue 0 * Q.eigenfunction 0 x := by
-  simp only [schrodingerOperator, one_div]
-  rw [deriv_deriv_eigenfunction_zero, eigenValue]
-  have hm' := Complex.ofReal_ne_zero.mpr Q.m_ne_zero
-  have hℏ' := Complex.ofReal_ne_zero.mpr Q.ℏ_ne_zero
-  field_simp
-  ring
+  simp
 
 lemma deriv_physHermite_succ (n : ℕ) :
-    deriv (fun x => Complex.ofReal (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x))) = fun x =>
-    Complex.ofReal (√(Q.m * Q.ω / Q.ℏ)) * 2 * (n + 1) * physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) := by
+    deriv (fun x => Complex.ofReal (physHermite (n + 1) (x/Q.ξ))) = fun x =>
+    Complex.ofReal (1/Q.ξ) * 2 * (n + 1) * physHermite n (x/Q.ξ) := by
   funext x
   trans deriv (Complex.ofReal ∘ physHermite (n + 1) ∘
-    fun (x : ℝ) => (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) x
-  · rfl
+    fun (x : ℝ) => ((1/Q.ξ) * x)) x
+  · congr
+    funext x
+    simp only [one_div, Function.comp_apply, Complex.ofReal_inj]
+    ring_nf
   rw [fderiv_comp_deriv _ (by fun_prop) (by fun_prop)]
   rw [fderiv_comp_deriv _ (by fun_prop) (by fun_prop)]
   simp only [Function.comp_apply, fderiv_eq_smul_deriv, smul_eq_mul, Complex.deriv_ofReal,
@@ -110,13 +104,13 @@ lemma deriv_physHermite_succ (n : ℕ) :
     Complex.ofReal_mul, Complex.ofReal_ofNat, Complex.ofReal_add, Complex.ofReal_natCast,
     Complex.ofReal_one]
   simp only [cast_add, cast_one, add_tsub_cancel_right]
-  ring
+  ring_nf
 
 lemma deriv_eigenfunction_succ (n : ℕ) :
-    deriv (Q.eigenfunction (n + 1)) = fun x => Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1)!)) •
-    (((√(Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1) * physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)
-      + physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x) * (-(Q.m * Q.ω) / Q.ℏ * ↑x))
-      * Q.eigenfunction 0 x) := by
+    deriv (Q.eigenfunction (n + 1)) = fun x =>
+    Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1)!) * (1/Q.ξ)) •
+    ((2 * (n + 1) * physHermite n (x/Q.ξ)
+      - (x/Q.ξ) * physHermite (n + 1) (x/Q.ξ)) * Q.eigenfunction 0 x) := by
   funext x
   rw [eigenfunction_eq_mul_eigenfunction_zero]
   rw [deriv_mul (by fun_prop) (by fun_prop)]
@@ -125,111 +119,123 @@ lemma deriv_eigenfunction_succ (n : ℕ) :
     Complex.ofReal_inv, differentiableAt_const, deriv_mul, deriv_const', zero_mul, mul_zero,
     add_zero, zero_add, smul_eq_mul]
   rw [deriv_physHermite_succ, deriv_eigenfunction_zero]
+  simp only [one_div, Complex.ofReal_inv, Complex.ofReal_div, Complex.ofReal_neg,
+    Complex.ofReal_one, Complex.ofReal_pow, Pi.mul_apply, Pi.smul_apply, smul_eq_mul, neg_mul,
+    mul_neg]
+  ring
+
+/-!
+
+## Second derivatives of the eigenfunctions.
+
+-/
+
+lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0)) x =
+    - (1/Q.ξ^2) * (Q.eigenfunction 0 x +
+    x * (- (1/Q.ξ^2) * x * Q.eigenfunction 0 x)) := by
+  simp only [deriv_eigenfunction_zero, neg_mul, Complex.ofReal_div, Complex.ofReal_neg,
+    Complex.ofReal_mul, Algebra.smul_mul_assoc]
+  trans deriv (fun x => (- (1/Q.ξ^2)) • (Complex.ofReal x * Q.eigenfunction 0 x)) x
+  · congr
+    funext x
+    simp only [Complex.ofReal_one, Complex.ofReal_pow, Pi.smul_apply, Pi.mul_apply, smul_eq_mul,
+      one_div, neg_smul, Complex.real_smul, Complex.ofReal_inv]
+    ring
+  simp only [Complex.real_smul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul,
+    differentiableAt_const, deriv_const_mul_field', mul_eq_mul_left_iff, div_eq_zero_iff,
+    neg_eq_zero, _root_.mul_eq_zero, Complex.ofReal_eq_zero]
+  rw [deriv_mul (by fun_prop) (by fun_prop)]
+  simp only [differentiableAt_const, deriv_const_mul_field', Complex.deriv_ofReal, mul_one]
+  rw [deriv_eigenfunction_zero]
   simp only [neg_mul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul, Pi.mul_apply,
     Pi.smul_apply, smul_eq_mul]
+  ring_nf
+  simp only [Complex.ofReal_one, Complex.ofReal_pow, one_mul, one_pow, inv_pow]
   ring
 
+
 lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) :
     deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
-    Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1) !)) *
-      ((↑√(Q.m * Q.ω / Q.ℏ) * 2 * (↑n + 1) *
-      deriv (fun x => ↑(physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) x +
-      (-(↑Q.m * ↑Q.ω) / ↑Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ) * (4 * (↑n + 1) * x) *
-      (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) +
-      (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-      (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x) := by
+    Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1) !) * (1/Q.ξ)) *
+      ((2 * (↑n + 1) * deriv (fun x => ↑(physHermite n (x/Q.ξ))) x +
+      (-(1/Q.ξ^2)) * (4 * (↑n + 1) * x) *
+      (physHermite n (x/Q.ξ)) + (- (1/Q.ξ)) * (1 + (- (1/Q.ξ^2)) * x ^ 2) *
+      (physHermite (n + 1) (x/Q.ξ))) * Q.eigenfunction 0 x) := by
   rw [deriv_eigenfunction_succ]
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
-    Complex.ofReal_inv, smul_eq_mul, differentiableAt_const, deriv_const_mul_field',
+    Complex.ofReal_inv, smul_eq_mul, differentiableAt_const, deriv_const_mul_field', neg_mul,
     mul_eq_mul_left_iff, _root_.mul_eq_zero, inv_eq_zero, Complex.ofReal_eq_zero, cast_nonneg,
     Real.sqrt_eq_zero, cast_eq_zero, ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false,
-    not_false_eq_true, pow_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
+    not_false_eq_true, pow_eq_zero_iff, OfNat.ofNat_ne_zero, or_false, ξ_ne_zero]
   left
   rw [deriv_mul (by fun_prop) (by fun_prop)]
   rw [deriv_eigenfunction_zero]
   simp only [← mul_assoc, neg_mul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul,
     Pi.mul_apply, Pi.smul_apply, smul_eq_mul, ← add_mul, mul_eq_mul_right_iff]
   left
-  rw [deriv_add (by fun_prop) (by fun_prop)]
+  rw [deriv_sub (by fun_prop) (by fun_prop)]
   rw [deriv_mul (by fun_prop) (by fun_prop)]
   simp only [differentiableAt_const, deriv_mul, deriv_const', zero_mul, mul_zero, add_zero,
     deriv_add, zero_add]
   rw [deriv_mul (by fun_prop) (by fun_prop)]
-  simp only [deriv_mul_const_field', Complex.deriv_ofReal, mul_one]
+  simp  [deriv_mul_const_field', Complex.deriv_ofReal, mul_one]
   rw [deriv_physHermite_succ]
-  simp only
+  ring_nf
+  simp only [one_div, Complex.ofReal_inv]
   ring
 
 lemma deriv_deriv_eigenfunction_one (x : ℝ) :
     deriv (fun x => deriv (Q.eigenfunction 1) x) x =
-      Complex.ofReal (1/Real.sqrt (2 ^ 1 * 1 !)) *
-      ((((-(Q.m * Q.ω) / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ) * (4 * x) +
-        (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-        (2 * (√(Q.m * Q.ω / Q.ℏ) * x)))) * Q.eigenfunction 0 x) := by
+      Complex.ofReal (1/Real.sqrt (2 ^ 1 * 1 !)  * (1/Q.ξ)) *
+      ((((- (1/ Q.ξ^2)) * (4 * x) + (- (1/ Q.ξ)) * (1 + (- (1/ Q.ξ^2)) * x ^ 2) *
+        (2 * ((1/ Q.ξ) * x)))) * Q.eigenfunction 0 x) := by
   rw [deriv_deriv_eigenfunction_succ]
   congr 2
-  simp [physHermite_one, Polynomial.aeval]
-
-lemma schrodingerOperator_eigenfunction_one (x : ℝ) :
-    Q.schrodingerOperator (Q.eigenfunction 1) x=
-    Q.eigenValue 1 * Q.eigenfunction 1 x := by
-  simp only [schrodingerOperator, one_div, eigenValue, cast_one, Complex.ofReal_mul,
-    Complex.ofReal_add, Complex.ofReal_one, Complex.ofReal_inv, Complex.ofReal_ofNat]
-  rw [deriv_deriv_eigenfunction_one]
-  have hm' := Complex.ofReal_ne_zero.mpr Q.m_ne_zero
-  have hℏ := Q.ℏ_ne_zero
-  have hℏ' := Complex.ofReal_ne_zero.mpr Q.ℏ_ne_zero
-  rw [Q.eigenfunction_eq_mul_eigenfunction_zero 1]
-  simp only [pow_one, factorial_one, cast_one, mul_one, one_div, Complex.ofReal_inv,
-    Polynomial.aeval, physHermite_one,
-    Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_mul, Polynomial.eval₂_ofNat, Polynomial.eval₂_X,
-    Complex.ofReal_mul, Complex.ofReal_ofNat]
+  simp only [CharP.cast_eq_zero, zero_add, mul_one, Polynomial.aeval, physHermite_zero, eq_intCast,
+    Int.cast_one, Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_one, Complex.ofReal_one,
+    deriv_const', mul_zero,  physHermite_one, Polynomial.eval₂_mul,
+    Polynomial.eval₂_ofNat, Polynomial.eval₂_X, Complex.ofReal_mul, Complex.ofReal_ofNat,
+    Complex.ofReal_div, add_right_inj, neg_inj, mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false,
+    _root_.mul_eq_zero, inv_eq_zero, Complex.ofReal_eq_zero]
   ring_nf
-  have hl : (Complex.ofReal √2 * Q.ℏ * (↑Q.m * ↑√2 * ↑Q.ℏ ^ 2)) ≠ 0 := by
-    simp_all
-  field_simp [hl, hℏ]
-  ring
+  left
+  trivial
 
 lemma deriv_deriv_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
-    deriv (fun x => deriv (Q.eigenfunction (n + 2)) x) x = (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 2)
-    + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2)) * Q.eigenfunction (n + 2) x := by
-  trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1 + 1) * (n + 1 + 1) !)) *
-        (((- Q.m * Q.ω / Q.ℏ) * (2 * (n + 2)
-        + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2)) *
-        (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x)
+    deriv (fun x => deriv (Q.eigenfunction (n + 2)) x) x = (- 1 / Q.ξ^2) * (2 * (n + 2)
+    + (1 + (- 1/ Q.ξ^2) * x ^ 2)) * Q.eigenfunction (n + 2) x := by
+  trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1 + 1) * (n + 1 + 1) !) ) *
+        (((- 1 / Q.ξ ^ 2) * (2 * (n + 2)
+        + (1 + (- 1/ Q.ξ ^ 2) * x ^ 2)) *
+        (physHermite (n + 2) (x/Q.ξ))) * Q.eigenfunction 0 x)
   · rw [deriv_deriv_eigenfunction_succ]
-    congr 2
-    trans (√(Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (√(Q.m * Q.ω / Q.ℏ) *
-      2 * (n + 1) * (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) +
-      (-(Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
-      (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
-      (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-      (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
+    rw [Complex.ofReal_mul, mul_assoc]
+    congr 1
+    rw [← mul_assoc]
+    congr 1
+    trans ((1 / Q.ξ) * 2 * (n + 1 + 1) * ((1 / Q.ξ) *
+      2 * (n + 1) * (physHermite n (x/Q.ξ))) +
+      (- (1 / Q.ξ^2)) * (1/Q.ξ) * (4 * (n + 1 + 1) * x) *
+      (physHermite (n + 1) (x/Q.ξ)) +
+      (- (1/Q.ξ^2)) * (1 + (-(1/Q.ξ^2)) * x ^ 2) *
+      (physHermite (n + 2) (x/Q.ξ)))
     · rw [deriv_physHermite_succ]
-      simp
-    trans ((Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (2 * (n + 1) *
-        (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) +
-        (- (Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
-        (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
-        (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-        (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-    · congr 2
-      trans (↑√(Q.m * Q.ω / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1 + 1) *
-      (2 * (↑n + 1) * ↑(physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)))
-      · ring
-      congr 3
-      rw [← Complex.ofReal_mul, ← Complex.ofReal_mul, ← Complex.ofReal_div]
-      congr 1
-      refine Real.mul_self_sqrt ?_
-      refine div_nonneg ?_ (le_of_lt Q.hℏ)
-      exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
-    trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) *
-          (2 * (√(Q.m * Q.ω / Q.ℏ) * x) * (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) -
-          2 * (n + 1) * (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)))
-          + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-    · ring
-    trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))
-          + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
+      simp only [one_div, Complex.ofReal_inv, cast_add, cast_one, neg_mul]
+      ring
+    trans ((1/ Q.ξ^2) * 2 * (n + 1 + 1) * (2 * (n + 1) *
+        (physHermite n (x/Q.ξ))) +
+        (- 1 / Q.ξ^2) * (1/Q.ξ) * (4 * (n + 1 + 1) * x) *
+        (physHermite (n + 1) (x/Q.ξ)) +
+        (- 1/ Q.ξ^2) * (1 + (- 1 / Q.ξ^2) * x ^ 2) *
+        (physHermite (n + 2) ((1/Q.ξ) * x)))
+    · ring_nf
+    trans (- 1/ Q.ξ^2) * (2 * (n + 1 + 1) *
+          (2 * ((1 / Q.ξ) * x) * (physHermite (n + 1) (x/Q.ξ)) -
+          2 * (n + 1) * (physHermite n (x/Q.ξ)))
+          + (1 + (- 1 / Q.ξ^2) * x ^ 2) * (physHermite (n + 2) ( x/Q.ξ)))
+    · ring_nf
+    trans (- 1 / Q.ξ^2) * (2 * (n + 1 + 1) * (physHermite (n + 2) (x/Q.ξ))
+          + (1 + (- 1/ Q.ξ^2) * x ^ 2) * (physHermite (n + 2) (x/Q.ξ)))
     · congr
       conv_rhs =>
         rw [physHermite_succ]
@@ -237,23 +243,38 @@ lemma deriv_deriv_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
         cast_one, map_sub, map_mul, Polynomial.aeval_X, map_add, map_natCast, map_one,
         Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_natCast,
         Complex.ofReal_one]
-      simp only [Polynomial.aeval, Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_ofNat,
-        Complex.ofReal_ofNat, sub_right_inj]
+      rw [show (Polynomial.aeval (x / Q.ξ)) 2 = 2 by simp [Polynomial.aeval]]
+      field_simp
       ring
     ring
   · rw [Q.eigenfunction_eq_mul_eigenfunction_zero (n + 2)]
     ring
 
-lemma schrodingerOperator_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
-    Q.schrodingerOperator (Q.eigenfunction (n + 2)) x=
-    Q.eigenValue (n + 2) * Q.eigenfunction (n + 2) x := by
-  simp only [schrodingerOperator, one_div, eigenValue, cast_add, cast_ofNat, Complex.ofReal_mul,
-    Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_ofNat, Complex.ofReal_inv]
-  rw [Q.deriv_deriv_eigenfunction_succ_succ]
-  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ℏ))
-  field_simp
-  ring
+lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) :
+    deriv (fun x => deriv (Q.eigenfunction n) x) x = (- 1 / Q.ξ^2) * ((2 * n + 1)
+    + ((- 1/ Q.ξ^2) * x ^ 2)) * Q.eigenfunction n x := by
+  match n with
+  | 0 =>
+    rw [deriv_deriv_eigenfunction_zero]
+    simp only [one_div, neg_mul, mul_neg, CharP.cast_eq_zero, mul_zero, zero_add]
+    ring
+  | 1 =>
+    rw [deriv_deriv_eigenfunction_one]
+    rw [Q.eigenfunction_eq_mul_eigenfunction_zero 1]
+    simp only [pow_one, factorial_one, cast_one, mul_one, one_div, Complex.ofReal_mul,
+      Complex.ofReal_inv, neg_mul, CharP.cast_eq_zero, zero_add, Polynomial.aeval, physHermite_one,
+      Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_mul, Polynomial.eval₂_ofNat,
+      Polynomial.eval₂_X, Complex.ofReal_ofNat, Complex.ofReal_div]
+    ring_nf
+  | n + 2 =>
+    rw [Q.deriv_deriv_eigenfunction_succ_succ n x]
+    simp only [cast_add, cast_one]
+    ring
+
+/-!
+
+## Application of the schrodingerOperator
+-/
 
 /-- 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,
@@ -262,13 +283,16 @@ lemma schrodingerOperator_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
 
   The proof of this result is done by explicit calculation of derivatives.
 -/
-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
+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
 
 open Filter Finset
 
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index 278c7482..08c64a2c 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -318,6 +318,7 @@ def harmonicOscillator : Note where
     .name ``QuantumMechanics.OneDimension.HilbertSpace.memHS_of_parity .complete,
     .h1 "The Schrodinger Operator",
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator .complete,
+    .name ``QuantumMechanics.OneDimension.HarmonicOscillator.ξ .complete,
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator .complete,
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity .complete,
     .h1 "The eigenfunctions of the Schrodinger Operator",