1d Reflectionless Potential

The quantum reflectionless potential in 1d. This file contains

• the definition of the reflectionless potential as defined https://arxiv.org/pdf/2411.14941
• properties of reflectionless potentials

TODO

• Define creation and annihilation operators for reflectionless potentials
• Write the proof of the general solution of the reflectionless potential using the creation and annihilation operators
• Show reflectionless properties

structure QuantumMechanics.OneDimension.ReflectionlessPotential : Type

A reflectionless potential is specified by three real parameters: the mass of the particle m, a value of Planck's constant ℏ, the parameter κ, as well as a positive integer family number N. All of these parameters are assumed to be positive. -

• m : ℝ

  mass of the particle

• κ : ℝ

  parameter of the reflectionless potential

• ℏ : ℝ

  Planck's constant

• N : ℕ

  family number, positive integer

• m_pos : 0 < self.m
• κ_pos : 0 < self.κ
• N_pos : 0 < self.N
• ℏ_pos : 0 < self.ℏ

Theorems

TODO: Add theorems about reflectionless potential - the main result is the actual 1d solution

noncomputable def QuantumMechanics.OneDimension.ReflectionlessPotential.reflectionlessPotential (Q : ReflectionlessPotential) (x : ℝ) : ℝ

Define the reflectionless potential as V(x) = - (ℏ^2 * κ^2 * N * (N + 1)) / (2 * m * (cosh (κ * x)) ^ 2) -

Equations

• Q.reflectionlessPotential x = -(Q.ℏ ^ 2 * Q.κ ^ 2 * ↑Q.N * (↑Q.N + 1)) / (2 * Q.m * Real.cosh (Q.κ * x) ^ 2)

noncomputable def QuantumMechanics.OneDimension.ReflectionlessPotential.tanhOperator (Q : ReflectionlessPotential) (ψ : ℝ → ℂ) : ℝ → ℂ

Define tanh(κ X) operator

Equations

• Q.tanhOperator ψ x = ↑(Real.tanh (Q.κ * x)) * ψ x

noncomputable def QuantumMechanics.OneDimension.ReflectionlessPotential.creationOperator (Q : ReflectionlessPotential) (ψ : ℝ → ℂ) : ℝ → ℂ

Creation operator: a† as defined in https://arxiv.org/pdf/2411.14941 a† = 1/√(2m) (P + iℏκ tanh(κX))

Equations

• Q.creationOperator ψ = fun (x : ℝ) => ↑(1 / √(2 * Q.m)) * (QuantumMechanics.OneDimension.momentumOperator ψ x + Complex.I * ↑Q.ℏ * ↑Q.κ * Q.tanhOperator ψ x)

noncomputable def QuantumMechanics.OneDimension.ReflectionlessPotential.annihilationOperator (Q : ReflectionlessPotential) (ψ : ℝ → ℂ) : ℝ → ℂ

Annihilation operator: a as defined in https://arxiv.org/pdf/2411.14941 a = 1/√(2m) (P - iℏκ tanh(κX))

Equations

• Q.annihilationOperator ψ = fun (x : ℝ) => ↑(1 / √(2 * Q.m)) * (QuantumMechanics.OneDimension.momentumOperator ψ x - Complex.I * ↑Q.ℏ * ↑Q.κ * Q.tanhOperator ψ x)