Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.Operators.OneDimension.Parity
public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum
public import Physlib.QuantumMechanics.Operators.OneDimension.Position

1d Harmonic Oscillator

The quantum harmonic oscillator in 1d. This file contains

the definition of the Schrodinger operator

the definition of eigenfunctions and eigenvalues of the Schrodinger operator in terms of Hermite polynomials

proof that eigenfunctions and eigenvalues are indeed eigenfunctions and eigenvalues.

TODO "Generalize 1d harmonic oscillator to d dimensions and SpaceDHilbertSpace."@[expose] public section

Some preliminary results about Complex.ofReal .

To be moved.

              lemma Complex.ofReal_hasDerivAt : HasDerivAt Complex.ofReal 1 x := byx:ℝ⊢ HasDerivAt ofReal 1 x
  let f1 : ℂ → ℂ := idx:ℝf1:ℂ → ℂ := id⊢ HasDerivAt ofReal 1 x
  change HasDerivAt (f1 ∘ Complex.ofReal) 1 xx:ℝf1:ℂ → ℂ := id⊢ HasDerivAt (f1 ∘ ofReal) 1 x
  apply HasDerivAt.comp_ofRealx:ℝf1:ℂ → ℂ := id⊢ HasDerivAt f1 1 ↑x
  simp only [f1]x:ℝf1:ℂ → ℂ := id⊢ HasDerivAt id 1 ↑x
  exact hasDerivAt_id _All goals completed! 🐙@[simp]
lemma Complex.deriv_ofReal : deriv Complex.ofReal x = 1 := byx:ℝ⊢ deriv ofReal x = 1
  exact HasDerivAt.deriv Complex.ofReal_hasDerivAtAll goals completed! 🐙@[fun_prop]
lemma Complex.differentiableAt_ofReal : DifferentiableAt ℝ Complex.ofReal x := byx:ℝ⊢ DifferentiableAt ℝ ofReal x
  exact HasFDerivAt.differentiableAt Complex.ofReal_hasDerivAtAll goals completed! 🐙

The 1d Harmonic Oscillator

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.

The mass of the particle.

The angular frequency of the harmonic oscillator.

              structure HarmonicOscillator where  m : ℝ  ω : ℝ
  hω : 0 < ω
  hm : 0 < m

              @[simp]
lemma m_pos : 0 < Q.m := Q.hm@[simp]
lemma m_nonneg : 0 ≤ Q.m := Q.hm.le@[simp]
lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne'@[simp]
lemma ω_pos : 0 < Q.ω := Q.hω@[simp]
lemma ω_nonneg : 0 ≤ Q.ω := Q.hω.le@[simp]
lemma ω_ne_zero : Q.ω ≠ 0 := Q.hω.ne'

The characteristic length

              lemma ξ_nonneg : 0 ≤ Q.ξ := Real.sqrt_nonneg _

@[simp]
lemma ξ_pos : 0 < Q.ξ := byQ:HarmonicOscillator⊢ 0 < Q.ξ
  rw [ξQ:HarmonicOscillator⊢ 0 < √(↑ℏ / (Q.m * Q.ω))Q:HarmonicOscillator⊢ 0 < √(↑ℏ / (Q.m * Q.ω))]Q:HarmonicOscillator⊢ 0 < √(↑ℏ / (Q.m * Q.ω))
  apply Real.sqrt_pos.mprQ:HarmonicOscillator⊢ 0 < ↑ℏ / (Q.m * Q.ω)
  apply div_poshaQ:HarmonicOscillator⊢ 0 < ↑ℏhbQ:HarmonicOscillator⊢ 0 < Q.m * Q.ω
  ·haQ:HarmonicOscillator⊢ 0 < ↑ℏ exact ℏ_posAll goals completed! 🐙
  ·hbQ:HarmonicOscillator⊢ 0 < Q.m * Q.ω exact mul_pos Q.hm Q.hωAll goals completed! 🐙@[simp]
lemma ξ_ne_zero : Q.ξ ≠ 0 := Ne.symm (_root_.ne_of_lt Q.ξ_pos)

lemma ξ_sq : Q.ξ^2 = ℏ / (Q.m * Q.ω) := byQ:HarmonicOscillator⊢ Q.ξ ^ 2 = ↑ℏ / (Q.m * Q.ω)
  rw [ξQ:HarmonicOscillator⊢ √(↑ℏ / (Q.m * Q.ω)) ^ 2 = ↑ℏ / (Q.m * Q.ω)Q:HarmonicOscillator⊢ √(↑ℏ / (Q.m * Q.ω)) ^ 2 = ↑ℏ / (Q.m * Q.ω)]Q:HarmonicOscillator⊢ √(↑ℏ / (Q.m * Q.ω)) ^ 2 = ↑ℏ / (Q.m * Q.ω)
  apply Real.sq_sqrtQ:HarmonicOscillator⊢ 0 ≤ ↑ℏ / (Q.m * Q.ω)
  apply div_nonneghaQ:HarmonicOscillator⊢ 0 ≤ ↑ℏhbQ:HarmonicOscillator⊢ 0 ≤ Q.m * Q.ω
  ·haQ:HarmonicOscillator⊢ 0 ≤ ↑ℏ exact ℏ_nonnegAll goals completed! 🐙
  ·hbQ:HarmonicOscillator⊢ 0 ≤ Q.m * Q.ω exact mul_nonneg (le_of_lt Q.hm) (le_of_lt Q.hω)All goals completed! 🐙@[simp]
lemma ξ_abs : abs Q.ξ = Q.ξ := abs_of_nonneg Q.ξ_nonneg

lemma one_over_ξ : 1/Q.ξ = √(Q.m * Q.ω / ℏ) := byQ:HarmonicOscillator⊢ 1 / Q.ξ = √(Q.m * Q.ω / ↑ℏ)
  have := ℏ_posQ:HarmonicOscillatorthis:0 < ↑ℏ⊢ 1 / Q.ξ = √(Q.m * Q.ω / ↑ℏ)
  simp only [ξ, one_div]Q:HarmonicOscillatorthis:0 < ↑ℏ⊢ (√(↑ℏ / (Q.m * Q.ω)))⁻¹ = √(Q.m * Q.ω / ↑ℏ)
  rw [← Real.sqrt_invQ:HarmonicOscillatorthis:0 < ↑ℏ⊢ √(↑ℏ / (Q.m * Q.ω))⁻¹ = √(Q.m * Q.ω / ↑ℏ)Q:HarmonicOscillatorthis:0 < ↑ℏ⊢ √(↑ℏ / (Q.m * Q.ω))⁻¹ = √(Q.m * Q.ω / ↑ℏ)]Q:HarmonicOscillatorthis:0 < ↑ℏ⊢ √(↑ℏ / (Q.m * Q.ω))⁻¹ = √(Q.m * Q.ω / ↑ℏ)
  field_simpAll goals completed! 🐙

lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / ℏ) := byQ:HarmonicOscillator⊢ Q.ξ⁻¹ = √(Q.m * Q.ω / ↑ℏ)
  rw [inv_eq_one_divQ:HarmonicOscillator⊢ 1 / Q.ξ = √(Q.m * Q.ω / ↑ℏ)Q:HarmonicOscillator⊢ 1 / Q.ξ = √(Q.m * Q.ω / ↑ℏ)]Q:HarmonicOscillator⊢ 1 / Q.ξ = √(Q.m * Q.ω / ↑ℏ)
  exact one_over_ξ QAll goals completed! 🐙

lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / ℏ := byQ:HarmonicOscillator⊢ (1 / Q.ξ) ^ 2 = Q.m * Q.ω / ↑ℏ
  rw [one_over_ξQ:HarmonicOscillator⊢ √(Q.m * Q.ω / ↑ℏ) ^ 2 = Q.m * Q.ω / ↑ℏQ:HarmonicOscillator⊢ √(Q.m * Q.ω / ↑ℏ) ^ 2 = Q.m * Q.ω / ↑ℏ]Q:HarmonicOscillator⊢ √(Q.m * Q.ω / ↑ℏ) ^ 2 = Q.m * Q.ω / ↑ℏ
  exact Real.sq_sqrt (byQ:HarmonicOscillator⊢ 0 ≤ Q.m * Q.ω / ↑ℏ simp [div_nonneg]All goals completed! 🐙)@[inherit_doc momentumOperator]
scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Pᵒᵖ" => momentumOperator@[inherit_doc positionOperator]
scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Xᵒᵖ" => positionOperatorlemma schrodingerOperator_eq (ψ : ℝ → ℂ) :
    Q.schrodingerOperator ψ = (- ℏ ^ 2 / (2 * Q.m)) •
    (deriv (deriv ψ)) + (1/2 * Q.m * Q.ω^2) • ((fun x => Complex.ofReal x ^2) * ψ) := byQ:HarmonicOscillatorψ:ℝ → ℂ⊢ Q.schrodingerOperator ψ = (-↑ℏ ^ 2 / (2 * Q.m)) • deriv (deriv ψ) + (1 / 2 * Q.m * Q.ω ^ 2) • ((fun x => ↑x ^ 2) * ψ)
  funext xQ:HarmonicOscillatorψ:ℝ → ℂx:ℝ⊢ Q.schrodingerOperator ψ x =
  ((-↑ℏ ^ 2 / (2 * Q.m)) • deriv (deriv ψ) + (1 / 2 * Q.m * Q.ω ^ 2) • ((fun x => ↑x ^ 2) * ψ)) 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]Q:HarmonicOscillatorψ:ℝ → ℂx:ℝ⊢ 2⁻¹ * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x = 2⁻¹ * ↑Q.m * ↑Q.ω ^ 2 * (↑x ^ 2 * ψ x)
  ringAll goals completed! 🐙

The schrodinger operator written in terms of ξ.

lemma schrodingerOperator_eq_ξ (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ =
    fun x => (ℏ ^2 / (2 * Q.m)) * (- (deriv (deriv ψ) x) + (1/Q.ξ^2)^2 * x^2 * ψ x) := byQ:HarmonicOscillatorψ:ℝ → ℂ⊢ Q.schrodingerOperator ψ = fun x => ↑↑ℏ ^ 2 / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (1 / ↑Q.ξ ^ 2) ^ 2 * ↑x ^ 2 * ψ x)
  funext xQ:HarmonicOscillatorψ:ℝ → ℂx:ℝ⊢ Q.schrodingerOperator ψ x = ↑↑ℏ ^ 2 / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (1 / ↑Q.ξ ^ 2) ^ 2 * ↑x ^ 2 * ψ x)
  simp [schrodingerOperator_eq, ξ_sq, ← Complex.ofReal_pow]Q:HarmonicOscillatorψ:ℝ → ℂx:ℝ⊢ -↑(↑ℏ ^ 2) / (2 * ↑Q.m) * deriv (deriv ψ) x + 2⁻¹ * ↑Q.m * ↑(Q.ω ^ 2) * (↑(x ^ 2) * ψ x) =
  ↑(↑ℏ ^ 2) / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (↑Q.m * ↑Q.ω / ↑↑ℏ) ^ 2 * ↑(x ^ 2) * ψ x)
  have := Complex.ofReal_ne_zero.mpr Q.m_ne_zeroQ:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:↑Q.m ≠ 0⊢ -↑(↑ℏ ^ 2) / (2 * ↑Q.m) * deriv (deriv ψ) x + 2⁻¹ * ↑Q.m * ↑(Q.ω ^ 2) * (↑(x ^ 2) * ψ x) =
  ↑(↑ℏ ^ 2) / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (↑Q.m * ↑Q.ω / ↑↑ℏ) ^ 2 * ↑(x ^ 2) * ψ x)
  have := Complex.ofReal_ne_zero.mpr ℏ_ne_zeroQ:HarmonicOscillatorψ:ℝ → ℂx:ℝthis✝:↑Q.m ≠ 0this:↑↑ℏ ≠ 0⊢ -↑(↑ℏ ^ 2) / (2 * ↑Q.m) * deriv (deriv ψ) x + 2⁻¹ * ↑Q.m * ↑(Q.ω ^ 2) * (↑(x ^ 2) * ψ x) =
  ↑(↑ℏ ^ 2) / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (↑Q.m * ↑Q.ω / ↑↑ℏ) ^ 2 * ↑(x ^ 2) * ψ x)
  field_simpQ:HarmonicOscillatorψ:ℝ → ℂx:ℝthis✝:↑Q.m ≠ 0this:↑↑ℏ ≠ 0⊢ (-(↑(↑ℏ ^ 2) * deriv (deriv ψ) x) + ↑Q.m ^ 2 * ↑(Q.ω ^ 2) * ↑(x ^ 2) * ψ x) * ↑↑ℏ ^ 2 =
  ↑(↑ℏ ^ 2) * (-(deriv (deriv ψ) x * ↑↑ℏ ^ 2) + ↑Q.m ^ 2 * ↑(x ^ 2) * ψ x * ↑Q.ω ^ 2)
  simp only [Complex.ofReal_pow]Q:HarmonicOscillatorψ:ℝ → ℂx:ℝthis✝:↑Q.m ≠ 0this:↑↑ℏ ≠ 0⊢ (-(↑↑ℏ ^ 2 * deriv (deriv ψ) x) + ↑Q.m ^ 2 * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) * ↑↑ℏ ^ 2 =
  ↑↑ℏ ^ 2 * (-(deriv (deriv ψ) x * ↑↑ℏ ^ 2) + ↑Q.m ^ 2 * ↑x ^ 2 * ψ x * ↑Q.ω ^ 2)
  ringAll goals completed! 🐙

The Schrodinger operator commutes with the parity operator.


lemma schrodingerOperator_parity (ψ : ℝ → ℂ) :
    Q.schrodingerOperator (parityOperator ψ) = parityOperator (Q.schrodingerOperator ψ) := byQ:HarmonicOscillatorψ:ℝ → ℂ⊢ Q.schrodingerOperator (parityOperator ψ) = parityOperator (Q.schrodingerOperator ψ)
  funext xQ:HarmonicOscillatorψ:ℝ → ℂx:ℝ⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) x
  have (ψ : ℝ → ℂ) : (fun x => (deriv fun x => ψ (-x)) x) = fun x => - deriv ψ (-x) := byQ:HarmonicOscillatorψ:ℝ → ℂ⊢ Q.schrodingerOperator (parityOperator ψ) = parityOperator (Q.schrodingerOperator ψ)Q:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:∀ (ψ : ℝ → ℂ), (fun x => deriv (fun x => ψ (-x)) x) = fun x => -deriv ψ (-x)⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) x
    funext xQ:HarmonicOscillatorψ✝:ℝ → ℂx✝:ℝψ:ℝ → ℂx:ℝ⊢ deriv (fun x => ψ (-x)) x = -deriv ψ (-x)Q:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:∀ (ψ : ℝ → ℂ), (fun x => deriv (fun x => ψ (-x)) x) = fun x => -deriv ψ (-x)⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) x
    rw [← deriv_comp_negQ:HarmonicOscillatorψ✝:ℝ → ℂx✝:ℝψ:ℝ → ℂx:ℝ⊢ deriv (fun x => ψ (-x)) x = deriv (fun x => ψ (-x)) xQ:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:∀ (ψ : ℝ → ℂ), (fun x => deriv (fun x => ψ (-x)) x) = fun x => -deriv ψ (-x)⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) x]Q:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:∀ (ψ : ℝ → ℂ), (fun x => deriv (fun x => ψ (-x)) x) = fun x => -deriv ψ (-x)⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) xQ:HarmonicOscillatorψ:ℝ → ℂx:ℝthis:∀ (ψ : ℝ → ℂ), (fun x => deriv (fun x => ψ (-x)) x) = fun x => -deriv ψ (-x)⊢ Q.schrodingerOperator (parityOperator ψ) x = parityOperator (Q.schrodingerOperator ψ) x
  simp [schrodingerOperator, parityOperator, this]All goals completed! 🐙

The Schrodinger operator is additive.


lemma schrodingerOperator_add (ψ φ : ℝ → ℂ)
    (hψ : Differentiable ℝ ψ) (hψ' : Differentiable ℝ (deriv ψ))
    (hφ : Differentiable ℝ φ) (hφ' : Differentiable ℝ (deriv φ)) :
    Q.schrodingerOperator (ψ + φ) = Q.schrodingerOperator ψ + Q.schrodingerOperator φ := byQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)⊢ Q.schrodingerOperator (ψ + φ) = Q.schrodingerOperator ψ + Q.schrodingerOperator φ
  unfold schrodingerOperatorQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)⊢ (fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x) =
  (fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
    -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x
  funext xQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
  have h_deriv_add : deriv (ψ + φ) = deriv ψ + deriv φ := byQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)⊢ Q.schrodingerOperator (ψ + φ) = Q.schrodingerOperator ψ + Q.schrodingerOperator φQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
    funext yQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝy:ℝ⊢ deriv (ψ + φ) y = (deriv ψ + deriv φ) yQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
    exact deriv_add (hψ y) (hφ y)Q:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    xQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (ψ + φ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
  rw [h_deriv_addQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ + deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    xQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ + deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x]Q:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ + deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
  rw [deriv_add (hψ' x) (hφ' x)Q:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * (deriv (deriv ψ) x + deriv (deriv φ) x) + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    xQ:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * (deriv (deriv ψ) x + deriv (deriv φ) x) + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x]Q:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * (deriv (deriv ψ) x + deriv (deriv φ) x) + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ + φ) x =
  ((fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) + fun x =>
      -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
    x
  simp only [Pi.add_apply]Q:HarmonicOscillatorψ:ℝ → ℂφ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)hφ:Differentiable ℝ φhφ':Differentiable ℝ (deriv φ)x:ℝh_deriv_add:deriv (ψ + φ) = deriv ψ + deriv φ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * (deriv (deriv ψ) x + deriv (deriv φ) x) + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (ψ x + φ x) =
  -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x +
    (-↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv φ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * φ x)
  ringAll goals completed! 🐙

The Schrodinger operator is homogeneous.


lemma schrodingerOperator_smul (c : ℂ) (ψ : ℝ → ℂ)
    (hψ : Differentiable ℝ ψ) (hψ' : Differentiable ℝ (deriv ψ)) :
    Q.schrodingerOperator (c • ψ) = c • Q.schrodingerOperator ψ := byQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)⊢ Q.schrodingerOperator (c • ψ) = c • Q.schrodingerOperator ψ
  unfold schrodingerOperatorQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)⊢ (fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x) =
  c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x
  funext xQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
  have h_deriv_smul : deriv (c • ψ) = c • deriv ψ := byQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)⊢ Q.schrodingerOperator (c • ψ) = c • Q.schrodingerOperator ψQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
    funext yQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝy:ℝ⊢ deriv (c • ψ) y = (c • deriv ψ) yQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
    exact deriv_const_smul c (hψ y)Q:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) xQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv (c • ψ)) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
  rw [h_deriv_smulQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (c • deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) xQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (c • deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x]Q:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (c • deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
  rw [deriv_const_smul c (hψ' x)Q:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * c • deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) xQ:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * c • deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x]Q:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * c • deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c • ψ) x =
  (c • fun x => -↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x) x
  simp only [Pi.smul_apply, smul_eq_mul]Q:HarmonicOscillatorc:ℂψ:ℝ → ℂhψ:Differentiable ℝ ψhψ':Differentiable ℝ (deriv ψ)x:ℝh_deriv_smul:deriv (c • ψ) = c • deriv ψ⊢ -↑↑ℏ ^ 2 / (2 * ↑Q.m) * (c * deriv (deriv ψ) x) + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * (c * ψ x) =
  c * (-↑↑ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x)
  ringAll goals completed! 🐙