PhysLean Documentation

PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic

1d Harmonic Oscillator #

The quantum harmonic oscillator in 1d. This file contains

TODO #

Some preliminary results about Complex.ofReal . #

To be moved.

source
theorem Complex.ofReal_hasDerivAt {x : ℝ} :
HasDerivAt ofReal 1 x
source
@[simp]
theorem Complex.deriv_ofReal {x : ℝ} :
deriv ofReal x = 1
source
theorem Complex.differentiableAt_ofReal {x : ℝ} :
DifferentiableAt ℝ ofReal x

The 1d Harmonic Oscillator

source
structure QuantumMechanics.OneDimension.HarmonicOscillator :
Type

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.

  • m : ℝ

    The mass of the particle.

  • ω : ℝ

    The angular frequency of the harmonic oscillator.

  • hω : 0 < self.ω
  • hm : 0 < self.m
Instances For
    source
    @[simp]
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_two_ℏ_pos (Q : HarmonicOscillator) :
    0 < Q.m * Q.ω / (2 * ↑Constants.ℏ)
    source
    @[simp]
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_ℏ_pos (Q : HarmonicOscillator) :
    0 < Q.m * Q.ω / ↑Constants.ℏ
    source
    theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_ne_zero (Q : HarmonicOscillator) :
    Q.m ≠ 0

    The characteristic length #

    source
    noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.ξ (Q : HarmonicOscillator) :
    ℝ

    The characteristic length ξ of the harmonic oscillator is defined as √(ℏ /(m ω)).

    Equations
    Instances For
      source
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_nonneg (Q : HarmonicOscillator) :
      0 ≤ Q.ξ
      source
      @[simp]
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_pos (Q : HarmonicOscillator) :
      0 < Q.ξ
      source
      @[simp]
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_ne_zero (Q : HarmonicOscillator) :
      Q.ξ ≠ 0
      source
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_sq (Q : HarmonicOscillator) :
      Q.ξ ^ 2 = ↑Constants.ℏ / (Q.m * Q.ω)
      source
      @[simp]
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_abs (Q : HarmonicOscillator) :
      |Q.ξ| = Q.ξ
      source
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ (Q : HarmonicOscillator) :
      1 / Q.ξ = √(Q.m * Q.ω / ↑Constants.ℏ)
      source
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_inverse (Q : HarmonicOscillator) :
      Q.ξ⁻¹ = √(Q.m * Q.ω / ↑Constants.ℏ)
      source
      theorem QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ_sq (Q : HarmonicOscillator) :
      (1 / Q.ξ) ^ 2 = Q.m * Q.ω / ↑Constants.ℏ
      source
      def QuantumMechanics.OneDimension.HarmonicOscillator.«termPᵒᵖ» :
      Lean.ParserDescr

      The momentum operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to - i ℏ ψ'.

      Equations
      Instances For
        source
        def QuantumMechanics.OneDimension.HarmonicOscillator.«termXᵒᵖ» :
        Lean.ParserDescr

        The position operator is defined as the linear map from ℝ → ℂ to ℝ → ℂ taking ψ to x * ψ.

        Equations
        Instances For
          source
          noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator (Q : HarmonicOscillator) (ψ : ℝ → ℂ) :
          ℝ → ℂ

          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 * ψ.

          Equations
          Instances For
            source
            theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq (Q : HarmonicOscillator) (ψ : ℝ → ℂ) :
            Q.schrodingerOperator ψ = (-↑Constants.ℏ ^ 2 / (2 * Q.m)) • deriv (deriv ψ) + (1 / 2 * Q.m * Q.ω ^ 2) • ((fun (x : ℝ) => ↑x ^ 2) * ψ)
            source
            theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq_ξ (Q : HarmonicOscillator) (ψ : ℝ → ℂ) :
            Q.schrodingerOperator ψ = fun (x : ℝ) => ↑↑Constants.ℏ ^ 2 / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (1 / ↑Q.ξ ^ 2) ^ 2 * ↑x ^ 2 * ψ x)

            The schrodinger operator written in terms of ξ.

            source
            theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity (Q : HarmonicOscillator) (ψ : ℝ → ℂ) :
            Q.schrodingerOperator (HilbertSpace.parityOperator ψ) = HilbertSpace.parityOperator (Q.schrodingerOperator ψ)

            The Schrodinger operator commutes with the parity operator.

            source
            theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_add (Q : HarmonicOscillator) (ψ φ : ℝ → ℂ) (hψ : Differentiable ℝ ψ) (hψ' : Differentiable ℝ (deriv ψ)) (hφ : Differentiable ℝ φ) (hφ' : Differentiable ℝ (deriv φ)) :
            Q.schrodingerOperator (ψ + φ) = Q.schrodingerOperator ψ + Q.schrodingerOperator φ

            The Schrodinger operator is additive.

            source
            theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_smul (Q : HarmonicOscillator) (c : ℂ) (ψ : ℝ → ℂ) (hψ : Differentiable ℝ ψ) (hψ' : Differentiable ℝ (deriv ψ)) :
            Q.schrodingerOperator (c • ψ) = c • Q.schrodingerOperator ψ

            The Schrodinger operator is homogeneous.