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.QuantumMechanics.Operators.Momentum
public import Physlib.QuantumMechanics.Operators.Multiplication
Single-particle quantum system on Space d
i. Overview
In this module we introduce the general notion of a single-particle quantum system on Space d.
The structure SpaceDQuantumSystem encompasses the basic information needed to specify the system,
namely the number of spatial dimensions, the particle's mass and the potential function.
ii. Key results
iii. Table of contents
A. Basic properties
B. Operators
B.1. Kinetic energy
B.2. Potential energy
B.3. Hamiltonian
iv. References
@[expose] public section
A single-particle quantum system with Hilbert space SpaceDHilbertSpace d,
characterized by the number of spatial dimensions d : ℕ, particle's mass m > 0
and potential function potential : Space d → ℝ.
The number of spatial dimensions.
The mass (positive).
The potential function.
The Hilbert space, SpaceDHilbertSpace Q.d.
abbrev HS := SpaceDHilbertSpace Q.dA. 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. Operators
B.1. Kinetic energy
The kinetic operator (2m)⁻¹𝐩² as a continuous linear map on Schwartz space.
lemma kineticCLM_eq : Q.kineticCLM = (2 * Q.m)⁻¹ • (𝐩 ⬝ᵥ 𝐩) := rfl
The kinetic operator as an unbounded operator with domain schwartzSubmodule Q.d.
def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := ofReal (2 * Q.m)⁻¹ • momentumSqOperatorlemma kineticOperator_eq : Q.kineticOperator = ofReal (2 * Q.m)⁻¹ • momentumSqOperator := rflB.2. Potential energy
The potential operator as a continuous linear map on Schwartz space,
where Q.potential is a function of temperate growth.
lemma potentialCLM_eq : Q.potentialCLM = smulLeftCLM ℂ (ofReal ∘ Q.potential) := rflQ:SpaceDQuantumSystemh_HTG:Function.HasTemperateGrowth Q.potentialψ:𝓢(Space Q.d, ℂ)⊢ (fun x => (ofReal ∘ Q.potential) x • ψ x) = fun x => Q.potential x • ψ x
All goals completed! 🐙All goals completed! 🐙
The potential operator as a self-adjoint, unbounded multiplication operator
with domain {ψ ∈ Q.HS | Q.potential • ψ ∈ Q.HS}.
lemma potentialOperator_eq : Q.potentialOperator = 𝓜 volume (ofReal ∘ Q.potential) := rfllemma potentialOperator_isSelfAdjoint (h_AESM : AEStronglyMeasurable Q.potential) :
IsSelfAdjoint Q.potentialOperator :=
mulOperator_isSelfAdjoint_ofReal (Q:SpaceDQuantumSystemh_AESM:AEStronglyMeasurable Q.potential volume⊢ AEStronglyMeasurable (ofReal ∘ Q.potential) volume All goals completed! 🐙) (Q:SpaceDQuantumSystemh_AESM:AEStronglyMeasurable Q.potential volume⊢ ⇑(starRingEnd ℂ) ∘ ofReal ∘ Q.potential = ofReal ∘ Q.potential Q:SpaceDQuantumSystemh_AESM:AEStronglyMeasurable Q.potential volumex✝:Space Q.d⊢ (⇑(starRingEnd ℂ) ∘ ofReal ∘ Q.potential) x✝ = (ofReal ∘ Q.potential) x✝; All goals completed! 🐙)lemma potentialOperator_domain_ge (h_HTG : Q.potential.HasTemperateGrowth) :
SchwartzSubmodule Q.d ≤ Q.potentialOperator.domain :=
mulOperator_domain_ge_of_hasTemperateGrowth (Q:SpaceDQuantumSystemh_HTG:Function.HasTemperateGrowth Q.potential⊢ Function.HasTemperateGrowth (ofReal ∘ Q.potential) All goals completed! 🐙) volumeB.3. Hamiltonian
The Hamiltonian operator as a continuous linear map on Schwartz space,
where Q.potential is a function of temperate growth.
def hamiltonianCLM : 𝓢(Space Q.d, ℂ) →L[ℂ] 𝓢(Space Q.d, ℂ) := Q.kineticCLM + Q.potentialCLMlemma hamiltonianCLM_eq : Q.hamiltonianCLM = Q.kineticCLM + Q.potentialCLM := rflThe Hamilontian operator as a symmetric unbounded operator.
def hamiltonianOperator : Q.HS →ₗ.[ℂ] Q.HS := Q.kineticOperator + Q.potentialOperatorlemma hamiltonianOperator_eq : Q.hamiltonianOperator = Q.kineticOperator + Q.potentialOperator :=
rfl