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.Unbounded
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule
public import Physlib.QuantumMechanics.PlanckConstant
public import Physlib.SpaceAndTime.Space.Derivatives.Basic
import Mathlib.Analysis.Calculus.FDeriv.StarMomentum operators
i. Overview
In this module we introduce several momentum operators for quantum mechanics on Space d.
ii. Key results
Definitions:
momentumCLM : (components of) the momentum vector operator acting on Schwartz maps
𝓢(Space d, ℂ) as -iℏ∂ᵢ.
momentumOperator : a symmetric unbounded operator acting on the Schwartz submodule
of the Hilbert space SpaceDHilbertSpace d.
Notation:
𝐩 for momentumOperator
iii. Table of contents
A. Momentum vector operator
B. Unbounded momentum vector operator
iv. References
TODO "Extend the domain of the momentum operator to the Sobolev space `H¹`."TODO "Prove that the momentum operator is self-adjoint (relies on 15310236534648318597)."@[expose] public sectionA. Momentum vector operator
Component i of the momentum operator is the continuous linear map
from 𝓢(Space d, ℂ) to itself which maps ψ to -iℏ ∂ᵢψ.
def momentumCLM : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) :=
(- Complex.I * ℏ) • (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis i)) ∘L
(SchwartzMap.fderivCLM ℂ (Space d) ℂ)@[inherit_doc momentumCLM]
notation "𝐩" => momentumCLM@[inherit_doc momentumCLM]
notation "𝐩[" d' "]" => momentumCLM (d := d')lemma momentumCLM_apply_fun (ψ : 𝓢(Space d, ℂ)) : 𝐩 i ψ = (-I * ℏ) • ∂[i] ψ := rfl@[simp]
lemma momentumCLM_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐩 i ψ x = -I * ℏ * ∂[i] ψ x :=
rflB. Unbounded momentum vector operator
The momentum operator as a LinearPMap with domain the Schwartz submodule.
def momentumOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d where
domain := SchwartzSubmodule d
toFun := (schwartzIncl volume).1 ∘ₗ (𝐩 i).1 ∘ₗ (schwartzEquiv volume).symm.1@[inherit_doc momentumOperator]
notation "𝓟" => momentumOperatorlemma momentumOperator_apply (ψ : SchwartzSubmodule d) :
𝓟 i ψ = schwartzEquiv volume (𝐩 i ((schwartzEquiv volume).symm ψ)) := rfllemma momentumOperator_apply_ae (ψ : SchwartzSubmodule d) :
𝓟 i ψ =ᵐ[volume] 𝐩 i ((schwartzEquiv volume).symm ψ) :=
schwartzEquiv_coe_ae _lemma momentumOperator_range (ψ : SchwartzSubmodule d) : 𝓟 i ψ ∈ SchwartzSubmodule d := d:ℕi:Fin dψ:↥(SchwartzSubmodule d volume)⊢ ↑(𝓟 i) ψ ∈ SchwartzSubmodule d volume
All goals completed! 🐙lemma momentumOperator_hasDenseDomain : (𝓟 i).HasDenseDomain := SchwartzSubmodule.dense d _d:ℕi:Fin df:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)heq:∀ (x : Space d), fderiv ℝ (star ∘ ⇑f) x = ↑(starL' ℝ) ∘SL fderiv ℝ (⇑f) xhI₁:Integrable (fun x => star (f x)) volumehI₂:Integrable (fun x => (fderiv ℝ (⇑g) x) (basis i) * star (f x)) volumehI₃:Integrable (fun x => g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i)) volumehI₄:Integrable (fun x => g x * star (f x)) volume⊢ ∫ (x : Space d), (starRingEnd ℂ) (f x) * (-I * ↑↑ℏ * Space.deriv i (⇑g) x) ∂volume =
∫ (x : Space d), -(I * ↑↑ℏ) * ((fderiv ℝ (⇑g) x) (basis i) * star (f x))
All goals completed! 🐙
d:ℕi:Fin df:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)heq:∀ (x : Space d), fderiv ℝ (star ∘ ⇑f) x = ↑(starL' ℝ) ∘SL fderiv ℝ (⇑f) xhI₁:Integrable (fun x => star (f x)) volumehI₂:Integrable (fun x => (fderiv ℝ (⇑g) x) (basis i) * star (f x)) volumehI₃:Integrable (fun x => g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i)) volumehI₄:Integrable (fun x => g x * star (f x)) volume⊢ I * ↑↑ℏ * ∫ (x : Space d), g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i) =
I * ↑↑ℏ * -∫ (x : Space d), (fderiv ℝ (⇑g) x) (basis i) * star (f x)
d:ℕi:Fin df:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)heq:∀ (x : Space d), fderiv ℝ (star ∘ ⇑f) x = ↑(starL' ℝ) ∘SL fderiv ℝ (⇑f) xhI₁:Integrable (fun x => star (f x)) volumehI₂:Integrable (fun x => (fderiv ℝ (⇑g) x) (basis i) * star (f x)) volumehI₃:Integrable (fun x => g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i)) volumehI₄:Integrable (fun x => g x * star (f x)) volume⊢ ∫ (x : Space d), g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i) = -∫ (x : Space d), (fderiv ℝ (⇑g) x) (basis i) * star (f x)
exact integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable hI₂ hI₃ hI₄ (d:ℕi:Fin df:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)heq:∀ (x : Space d), fderiv ℝ (star ∘ ⇑f) x = ↑(starL' ℝ) ∘SL fderiv ℝ (⇑f) xhI₁:Integrable (fun x => star (f x)) volumehI₂:Integrable (fun x => (fderiv ℝ (⇑g) x) (basis i) * star (f x)) volumehI₃:Integrable (fun x => g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i)) volumehI₄:Integrable (fun x => g x * star (f x)) volume⊢ ∀ x ∈ tsupport (star ∘ ⇑f), DifferentiableAt ℝ (⇑g) x All goals completed! 🐙) (d:ℕi:Fin df:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)heq:∀ (x : Space d), fderiv ℝ (star ∘ ⇑f) x = ↑(starL' ℝ) ∘SL fderiv ℝ (⇑f) xhI₁:Integrable (fun x => star (f x)) volumehI₂:Integrable (fun x => (fderiv ℝ (⇑g) x) (basis i) * star (f x)) volumehI₃:Integrable (fun x => g x * (fderiv ℝ (star ∘ ⇑f) x) (basis i)) volumehI₄:Integrable (fun x => g x * star (f x)) volume⊢ ∀ x ∈ tsupport ⇑g, DifferentiableAt ℝ (star ∘ ⇑f) x All goals completed! 🐙)lemma momentumOperator_isUnbounded : (𝓟 i).IsUnbounded := d:ℕi:Fin d⊢ (𝓟 i).IsUnbounded
d:ℕi:Fin d⊢ (𝓟 i).IsSymmetricd:ℕi:Fin d⊢ (𝓟 i).HasDenseDomain
d:ℕi:Fin d⊢ (𝓟 i).IsSymmetric All goals completed! 🐙
d:ℕi:Fin d⊢ (𝓟 i).HasDenseDomain All goals completed! 🐙The square of the momentum operator.
def momentumSqOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d :=
sum fun i ↦ (𝓟 i).comp (𝓟 i) (momentumOperator_range i)lemma momentumSqOperator_eq :
momentumSqOperator (d := d) = sum fun i ↦ (𝓟 i).comp (𝓟 i) (momentumOperator_range i) := rfld:ℕhd:0 < dthis:Nonempty (Fin d) := ···⊢ ⨅ a, ((𝓟 a).comp (𝓟 a) ⋯).domain = ⨅ x, SchwartzSubmodule d volume
All goals completed! 🐙