Momentum operators

i. Overview

In this module we introduce several momentum operators for quantum mechanics on Space d.

ii. Key results

Definitions:

• momentumOperator : (components of) the momentum vector operator acting on Schwartz maps 𝓢(Space d, ℂ) as -iℏ∂ᵢ.
• momentumOperatorSqr : operator acting on Schwartz maps 𝓢(Space d, ℂ) as ∑ᵢ 𝐩[i]∘𝐩[i].
• momentumUnboundedOperator : a symmetric unbounded operator acting on the Schwartz submodule of the Hilbert space SpaceDHilbertSpace d.

Notation:

• 𝐩[i] for momentumOperator i
• 𝐩² for momentumOperatorSqr

iii. Table of contents

• A. Momentum vector operator
• B. Momentum-squared operator
• C. Unbounded momentum vector operator

iv. References

A. Momentum vector operator

def QuantumMechanics.momentumOperator {d : ℕ} (i : Fin d) : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ

Component i of the momentum operator is the continuous linear map from 𝓢(Space d, ℂ) to itself which maps ψ to -iℏ ∂ᵢψ.

Equations

• 𝐩[i] = (-Complex.I * ↑↑Constants.ℏ) • (SchwartzMap.evalCLM ℂ (Space d) ℂ (Space.basis i)).comp (SchwartzMap.fderivCLM ℂ (Space d) ℂ)

def QuantumMechanics.«term𝐩[_]» : Lean.ParserDescr

Component i of the momentum operator is the continuous linear map from 𝓢(Space d, ℂ) to itself which maps ψ to -iℏ ∂ᵢψ.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumMechanics.momentumOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : SchwartzMap (Space d) ℂ) : ⇑(𝐩[i] ψ) = (-Complex.I * ↑↑Constants.ℏ) • Space.deriv i ⇑ψ

@[simp]

theorem QuantumMechanics.momentumOperator_apply {d : ℕ} (i : Fin d) (ψ : SchwartzMap (Space d) ℂ) (x : Space d) : (𝐩[i] ψ) x = -Complex.I * ↑↑Constants.ℏ * Space.deriv i (⇑ψ) x

B. Momentum-squared operator

def QuantumMechanics.momentumOperatorSqr {d : ℕ} : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ

The square of the momentum operator, 𝐩² ≔ ∑ᵢ 𝐩ᵢ∘𝐩ᵢ.

Equations

• 𝐩² = ∑ i : Fin d, 𝐩[i].comp 𝐩[i]

def QuantumMechanics.«term𝐩²» : Lean.ParserDescr

The square of the momentum operator, 𝐩² ≔ ∑ᵢ 𝐩ᵢ∘𝐩ᵢ.

Equations

• QuantumMechanics.«term𝐩²» = Lean.ParserDescr.node `QuantumMechanics.«term𝐩²» 1024 (Lean.ParserDescr.symbol "𝐩²")

theorem QuantumMechanics.momentumOperatorSqr_apply {d : ℕ} (ψ : SchwartzMap (Space d) ℂ) (x : Space d) : (𝐩² ψ) x = ∑ i : Fin d, (𝐩[i] (𝐩[i] ψ)) x

C. Unbounded momentum vector operator

def QuantumMechanics.momentumOperatorSchwartz {d : ℕ} (i : Fin d) : ↥(SpaceDHilbertSpace.schwartzSubmodule d) →ₗ[ℂ] ↥(SpaceDHilbertSpace.schwartzSubmodule d)

The momentum operators defined on the Schwartz submodule.

Equations

• QuantumMechanics.momentumOperatorSchwartz i = ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv ∘ₗ ↑𝐩[i] ∘ₗ ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv.symm

theorem QuantumMechanics.momentumOperatorSchwartz_isSymmetric {d : ℕ} (i : Fin d) : (momentumOperatorSchwartz i).IsSymmetric

def QuantumMechanics.momentumUnboundedOperator {d : ℕ} (i : Fin d) : UnboundedOperator ↥(SpaceDHilbertSpace d) ↥(SpaceDHilbertSpace d)

The symmetric momentum unbounded operators with domain the Schwartz submodule of the Hilbert space.

Equations

• QuantumMechanics.momentumUnboundedOperator i = QuantumMechanics.UnboundedOperator.ofSymmetric ⋯ ⋯