The 1d QM system with general potential

noncomputable def QuantumMechanics.OneDimension.momentumOperator (ℏ : ℝ) (ψ : ℝ → ℂ) : ℝ → ℂ

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

The notation Pᵒᵖ can be used for the momentum operator.

Equations

• QuantumMechanics.OneDimension.momentumOperator ℏ ψ x = -Complex.I * ↑ℏ * deriv ψ x

theorem QuantumMechanics.OneDimension.momentumOperator_linear (ℏ : ℝ) (a1 a2 : ℂ) (ψ1 ψ2 : ℝ → ℂ) (hψ1_x : Differentiable ℝ ψ1) (hψ2_x : Differentiable ℝ ψ2) : momentumOperator ℏ (a1 • ψ1 + a2 • ψ2) = a1 • momentumOperator ℏ ψ1 + a2 • momentumOperator ℏ ψ2

theorem QuantumMechanics.OneDimension.momentumOperator_sq_linear (ℏ : ℝ) (a1 a2 : ℂ) (ψ1 ψ2 : ℝ → ℂ) (hψ1_x : Differentiable ℝ ψ1) (hψ2_x : Differentiable ℝ ψ2) (hψ1_xx : Differentiable ℝ (momentumOperator ℏ ψ1)) (hψ2_xx : Differentiable ℝ (momentumOperator ℏ ψ2)) : momentumOperator ℏ (momentumOperator ℏ (a1 • ψ1 + a2 • ψ2)) = a1 • momentumOperator ℏ (momentumOperator ℏ ψ1) + a2 • momentumOperator ℏ (momentumOperator ℏ ψ2)

noncomputable def QuantumMechanics.OneDimension.positionOperator (ψ : ℝ → ℂ) : ℝ → ℂ

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

Equations

• QuantumMechanics.OneDimension.positionOperator ψ x = ↑x * ψ x

noncomputable def QuantumMechanics.OneDimension.potentialOperator (V : ℝ → ℝ) (ψ : ℝ → ℂ) : ℝ → ℂ

The potential operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to V(x) ψ.

Equations

• QuantumMechanics.OneDimension.potentialOperator V ψ x = ↑(V x) * ψ x

theorem QuantumMechanics.OneDimension.potentialOperator_linear (V : ℝ → ℝ) (a1 a2 : ℂ) (ψ1 ψ2 : ℝ → ℂ) : potentialOperator V (a1 • ψ1 + a2 • ψ2) = a1 • potentialOperator V ψ1 + a2 • potentialOperator V ψ2

structure QuantumMechanics.OneDimension.GeneralPotential : Type

A quantum mechanical system in 1D is specified by a three real parameters: the mass of the particle m, a value of Planck's constant ℏ, and a potential function V

• m : ℝ

  The mass of the particle.

• ℏ : ℝ

  Reduced Planck's constant.

• V : ℝ → ℝ

  The potential.

• hℏ : 0 < self.ℏ
• hm : 0 < self.m

noncomputable def QuantumMechanics.OneDimension.GeneralPotential.schrodingerOperator (Q : GeneralPotential) (ψ : ℝ → ℂ) : ℝ → ℂ

For a 1D quantum mechanical system in potential V, the Schrodinger Operator corresponding to it is defined as the function from ℝ → ℂ to ℝ → ℂ taking

ψ ↦ - ℏ^2 / (2 * m) * ψ'' + V(x) * ψ.

Equations

• Q.schrodingerOperator ψ x = 1 / (2 * ↑Q.m) * QuantumMechanics.OneDimension.momentumOperator Q.ℏ (QuantumMechanics.OneDimension.momentumOperator Q.ℏ ψ) x + ↑(Q.V x) * ψ x

theorem QuantumMechanics.OneDimension.GeneralPotential.schrodingerOperator_linear (Q : GeneralPotential) (a1 a2 : ℂ) (ψ1 ψ2 : ℝ → ℂ) (hψ1_x : Differentiable ℝ ψ1) (hψ2_x : Differentiable ℝ ψ2) (hψ1_xx : Differentiable ℝ (momentumOperator Q.ℏ ψ1)) (hψ2_xx : Differentiable ℝ (momentumOperator Q.ℏ ψ2)) : Q.schrodingerOperator (a1 • ψ1 + a2 • ψ2) = a1 • Q.schrodingerOperator ψ1 + a2 • Q.schrodingerOperator ψ2