Physlib.QuantumMechanics.ReflectionlessPotential.Basic

Imports

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

public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum
public import Physlib.Mathematics.Trigonometry.Tanh
public import Physlib.Meta.TODO.Basic

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

              TODO "Refactor to use `SpaceDHilbertSpace 1`."TODO "Refactor to use `QuantumMechanics.PlanckConstant`."@[expose] public section

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

mass of the particle

parameter of the reflectionless potential

Planck's constant

family number, positive integer

              structure ReflectionlessPotential where  m : ℝ  κ : ℝ  ℏ : ℝ  N : ℕ
  m_pos : 0 < m -- mass of the particle is positive
  κ_pos : 0 < κ -- parameter of the reflectionless potential is positive
  N_pos : 0 < N -- family number is positive
  ℏ_pos : 0 < ℏ -- Planck's constant is positive

Theorems

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

-- First, you need a theorem that the scaled tanh has temperate growth
lemma scaled_tanh_hasTemperateGrowth (κ : ℝ) :
    Function.HasTemperateGrowth (fun x => (Real.tanh (κ * x))) :=
  tanh_const_mul_hasTemperateGrowth κ

This is a helper lemma to show that the embedding of a real function with temperate growth in ℂ also has temperate growth

private lemma complex_embedding_of_temperate_growth (f : ℝ → ℝ)
    (h : Function.HasTemperateGrowth f) : Function.HasTemperateGrowth (fun x => (f x : ℂ)) :=
  Function.Complex.hasTemperateGrowth_ofReal.comp h

-- Scaled tanh embedded into the complex numbers has temperate growth
lemma scaled_tanh_complex_hasTemperateGrowth (κ : ℝ) :
    Function.HasTemperateGrowth (fun x => (Real.tanh (κ * x) : ℂ)) :=
  complex_embedding_of_temperate_growth _ (scaled_tanh_hasTemperateGrowth κ)