The 1d QM system with general potential

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

• V : ℝ → ℝ

  The potential.

• 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 (QuantumMechanics.OneDimension.momentumOperator ψ) 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 ψ1)) (hψ2_xx : Differentiable ℝ (momentumOperator ψ2)) : Q.schrodingerOperator (a1 • ψ1 + a2 • ψ2) = a1 • Q.schrodingerOperator ψ1 + a2 • Q.schrodingerOperator ψ2