Imports
/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module
public import Physlib.Meta.Informal.Basic
public import Physlib.QuantumMechanics.Operators.Momentum
public import Physlib.QuantumMechanics.Operators.Multiplication
public import Physlib.QuantumMechanics.QuantumSystem.BasicThe rectangular potential barrier
i. Overview
The rectangular potential barrier in one dimension provides the simplest example of quantum
tunnelling. A particle of mass m is subject to a piece-wise constant potential which is Vβ
on a closed interval and zero elsewhere.
ii. Key results
iii. Table of contents
A. Basic properties
B. Potential function
C. Hilbert space
D. Operators
D.1. Kinetic
D.2. Potential
D.3. Hamiltonian
E. As a quantum system
iv. References
@[expose] public section
A quantum particle with mass m > 0 on Space 1 subject to a rectangular potential barrier.
The potential is Vβ on the interval Icc lower upper and zero elsewhere.
The mass (positive).
The lower bound of the barrier.
The upper bound of the barrier.
The height of the potential barrier.
structure RectangularBarrier where m : β
hm : 0 < m lower : β upper : β
h_bounds : lower < upper Vβ : βA. Basic properties
@[simp]
lemma m_pos : 0 < Q.m := Q.hm@[simp]
lemma m_nonneg : 0 β€ Q.m := Q.hm.le@[simp]
lemma m_ne_zero : Q.m β 0 := Q.hm.ne'B. Potential function
The piece-wise constant potential, equal to Q.Vβ for x.val 0 β Icc Q.lower Q.upper
and zero otherwise.
def potentialFunction : Space 1 β β := fun x β¦ (Icc Q.lower Q.upper).indicator (fun _ β¦ Q.Vβ) (x 0)lemma potentialFunction_eq :
Q.potentialFunction = fun x β¦ (Icc Q.lower Q.upper).indicator (fun _ β¦ Q.Vβ) (x 0) := rflThe piecewise-constant potential of the rectangular barrier is a.e. strongly measurable.
Q:RectangularBarrierhi:MeasurableSet (Icc Q.lower Q.upper)hf:Measurable fun x => x.val 0β’ MeasurableSet (Icc Q.lower Q.upper β fun x => x.val 0)
All goals completed! πC. Hilbert space
The Hilbert space for the 1d rectangular barrier.
@[nolint unusedArguments]
abbrev HS (_ : RectangularBarrier) : Type _ := SpaceDHilbertSpace 1D. Operators
D.1. Kinetic
The kinetic energy operator, pΒ²/2m.
def kineticOperator : Q.HS ββ.[β] Q.HS := (2 * Q.m)β»ΒΉ β’ momentumSqOperatorD.2. Potential
The potential energy operator, defined by multiplication by Q.potentialFunction.
def potentialOperator : Q.HS ββ.[β] Q.HS := π volume (Complex.ofReal β Q.potentialFunction)The potential operator for the rectangular barrier is self-adjoint.
Q:RectangularBarrierβ’ AEStronglyMeasurable (Complex.ofReal β Q.potentialFunction) volumeQ:RectangularBarrierβ’ β(starRingEnd β) β Complex.ofReal β Q.potentialFunction = Complex.ofReal β Q.potentialFunction
Q:RectangularBarrierβ’ β(starRingEnd β) β Complex.ofReal β Q.potentialFunction = Complex.ofReal β Q.potentialFunctionQ:RectangularBarrierβ’ AEStronglyMeasurable (Complex.ofReal β Q.potentialFunction) volume
Q:RectangularBarrierx:Space 1β’ (β(starRingEnd β) β Complex.ofReal β Q.potentialFunction) x = (Complex.ofReal β Q.potentialFunction) xQ:RectangularBarrierβ’ AEStronglyMeasurable (Complex.ofReal β Q.potentialFunction) volume
Q:RectangularBarrierβ’ AEStronglyMeasurable (Complex.ofReal β Q.potentialFunction) volume
Q:RectangularBarrierhQ:β (Q : RectangularBarrier), AEStronglyMeasurable Q.potentialFunction volumeβ’ AEStronglyMeasurable (Complex.ofReal β Q.potentialFunction) volume
All goals completed! πD.3. Hamiltonian
The Hamiltonian for the rectangular barrier.
informal_definition hamiltonian where
deps := [``RectangularBarrier]
tag := "QM-RB-ham"The Hamiltonian for the rectangular barrier is essentially self-adjoint.
informal_lemma hamiltonian_essentially_self_adjoint where
deps := [``RectangularBarrier.hamiltonian]
tag := "QM-RB-hamESA"E. As a quantum system
The rectangular barrier as a quantum system (self-adjoint Hamiltonian acting on a Hilbert space).
informal_definition toQuantumSystem where
deps := [``RectangularBarrier.hamiltonian_essentially_self_adjoint]
tag := "QM-RB-sys"