Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.PositionStates
public import Physlib.QuantumMechanics.Operators.OneDimension.Unbounded
public import Physlib.Mathematics.Distribution.PowMul
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.SchwartzSubmodulePosition operator
In this module we define:
The position operator on functions ℝ → ℂ
The position operator on Schwartz maps as an unbounded operator on the Hilbert space.
We show that position wavefunctions are generalized eigenvectors of the position operator.
@[expose] public section
The position operator on functions ℝ → ℂ
The position operator is defined as the linear map from ℝ → ℂ to ℝ → ℂ taking
ψ to x * ψ.
def positionOperator : (ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ where
toFun ψ := fun x ↦ x * ψ x
map_add' ψ1 ψ2 := ψ1:ℝ → ℂψ2:ℝ → ℂ⊢ (fun x => ↑x * (ψ1 + ψ2) x) = (fun x => ↑x * ψ1 x) + fun x => ↑x * ψ2 x
ψ1:ℝ → ℂψ2:ℝ → ℂx:ℝ⊢ ↑x * (ψ1 + ψ2) x = ((fun x => ↑x * ψ1 x) + fun x => ↑x * ψ2 x) x
ψ1:ℝ → ℂψ2:ℝ → ℂx:ℝ⊢ ↑x * (ψ1 x + ψ2 x) = ↑x * ψ1 x + ↑x * ψ2 x
All goals completed! 🐙
map_smul' a ψ1 := a:ℂψ1:ℝ → ℂ⊢ (fun x => ↑x * (a • ψ1) x) = (RingHom.id ℂ) a • fun x => ↑x * ψ1 x
a:ℂψ1:ℝ → ℂx:ℝ⊢ ↑x * (a • ψ1) x = ((RingHom.id ℂ) a • fun x => ↑x * ψ1 x) x
a:ℂψ1:ℝ → ℂx:ℝ⊢ ↑x * (a * ψ1 x) = a * (↑x * ψ1 x)
All goals completed! 🐙The position operator on Schwartz maps
The position operator on the Schwartz maps is defined as the linear map from
𝓢(ℝ, ℂ) to itself, such that ψ is taken to fun x => x * ψ x.
def positionOperatorSchwartz : 𝓢(ℝ, ℂ) →L[ℂ] 𝓢(ℝ, ℂ) := Distribution.powOneMul ℂlemma positionOperatorSchwartz_apply_fun (ψ : 𝓢(ℝ, ℂ)) :
(positionOperatorSchwartz ψ) = fun x => x * ψ x := ψ:𝓢(ℝ, ℂ)⊢ ⇑(positionOperatorSchwartz ψ) = fun x => ↑x * ψ x
ψ:𝓢(ℝ, ℂ)⊢ ⇑((Distribution.powOneMul ℂ) ψ) = fun x => ↑x * ψ x
All goals completed! 🐙@[simp]
lemma positionOperatorSchwartz_apply (ψ : 𝓢(ℝ, ℂ)) (x : ℝ) :
(positionOperatorSchwartz ψ) x = x * ψ x := ψ:𝓢(ℝ, ℂ)x:ℝ⊢ (positionOperatorSchwartz ψ) x = ↑x * ψ x
ψ:𝓢(ℝ, ℂ)x:ℝ⊢ ((Distribution.powOneMul ℂ) ψ) x = ↑x * ψ x
All goals completed! 🐙The unbounded position operator, whose domain is Schwartz maps.
def positionOperatorUnbounded : UnboundedOperator schwartzIncl schwartzIncl_injective :=
UnboundedOperator.ofSelfCLM positionOperatorSchwartzGeneralized eigenvectors of the momentum operator
x:ℝ⊢ ∀ (ψ : 𝓢(ℝ, ℂ)), (positionState x) (positionOperatorSchwartz ψ) = ↑x • (positionState x) ψ
x:ℝψ:𝓢(ℝ, ℂ)⊢ (positionState x) (positionOperatorSchwartz ψ) = ↑x • (positionState x) ψ
All goals completed! 🐙Position operator is symmetric
ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ ∫ (x : ℝ), (starRingEnd ℂ) ((positionOperatorSchwartz ψ1) x) * ψ2 x =
∫ (x : ℝ), (starRingEnd ℂ) (ψ1 x) * (positionOperatorSchwartz ψ2) x
ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)⊢ (fun x => (starRingEnd ℂ) ((positionOperatorSchwartz ψ1) x) * ψ2 x) = fun x =>
(starRingEnd ℂ) (ψ1 x) * (positionOperatorSchwartz ψ2) x
ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)x:ℝ⊢ (starRingEnd ℂ) ((positionOperatorSchwartz ψ1) x) * ψ2 x = (starRingEnd ℂ) (ψ1 x) * (positionOperatorSchwartz ψ2) x
ψ1:𝓢(ℝ, ℂ)ψ2:𝓢(ℝ, ℂ)x:ℝ⊢ ↑x * (starRingEnd ℂ) (ψ1 x) * ψ2 x = (starRingEnd ℂ) (ψ1 x) * (↑x * ψ2 x)
All goals completed! 🐙