Position operators

i. Overview

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

ii. Key results

Definitions:

• positionOperator : (components of) the position vector operator acting on Schwartz maps 𝓢(Space d, ℂ) by multiplication by xᵢ.
• radiusRegPowOperator : operator acting on Schwartz maps by multiplication by (‖x‖² + ε²)^(s/2), a smooth regularization of ‖x‖ˢ.
• positionUnboundedOperator : a symmetric unbounded operator acting on the Schwartz submodule of the Hilbert space SpaceDHilbertSpace d.
• readiusRegPowUnboundedOperator : a symmetric unbounded operator acting on the Schwartz submodule of the Hilbert space SpaceDHilbertSpace d. For s ≤ 0 this operator is in fact bounded (by |ε|ˢ) and has natural domain the entire Hilbert space, but for uniformity we use the same domain for all s.

Notation:

• 𝐱[i] for positionOperator i
• 𝐫[ε,s] for radiusRegPowOperator ε s

iii. Table of contents

• A. Position vector operator
• B. Regularized radius operator
• C. Unbounded position vector operator
• D. Unbounded regularized radius operator

iv. References

A. Position vector operator

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

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

Equations

• 𝐱[i] = SchwartzMap.smulLeftCLM ℂ ⇑(Complex.ofRealCLM.comp (Space.coordCLM i))

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

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

Equations

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

theorem QuantumMechanics.positionOperator_apply_fun {d : ℕ} (i : Fin d) (ψ : SchwartzMap (Space d) ℂ) : 𝐱[i] ψ = SchwartzMap.smulLeftCLM ℂ ⇑(Space.coordCLM i) • ψ

@[simp]

theorem QuantumMechanics.positionOperator_apply {d : ℕ} (i : Fin d) (ψ : SchwartzMap (Space d) ℂ) (x : Space d) : (𝐱[i] ψ) x = ↑(x.val i) * ψ x

B. Regularized radius operator

def QuantumMechanics.normRegularizedPow (d : ℕ) (ε s : ℝ) : Space d → ℝ

Power of regularized norm, (‖x‖² + ε²)^(s/2).

Equations

• QuantumMechanics.normRegularizedPow d ε s x = (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)

theorem QuantumMechanics.norm_sq_add_unit_sq_pos {d : ℕ} (ε : ℝˣ) (x : Space d) : 0 < ‖x‖ ^ 2 + ↑ε ^ 2

theorem QuantumMechanics.normRegularizedPow_pos (d : ℕ) (ε : ℝˣ) (s : ℝ) (x : Space d) : 0 < normRegularizedPow d (↑ε) s x

theorem QuantumMechanics.normRegularizedPow_hasTemperateGrowth (d : ℕ) (ε : ℝˣ) (s : ℝ) : Function.HasTemperateGrowth (normRegularizedPow d (↑ε) s)

def QuantumMechanics.radiusRegPowOperator {d : ℕ} (ε : ℝˣ) (s : ℝ) : SchwartzMap (Space d) ℂ →L[ℂ] SchwartzMap (Space d) ℂ

The radius operator to power s, regularized by ε ≠ 0, is the continuous linear map from 𝓢(Space d, ℂ) to itself which maps ψ to (‖x‖² + ε²)^(s/2) • ψ.

Equations

• 𝐫[ε,s] = SchwartzMap.smulLeftCLM ℂ (Complex.ofReal ∘ QuantumMechanics.normRegularizedPow d (↑ε) s)

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

The radius operator to power s, regularized by ε ≠ 0, is the continuous linear map from 𝓢(Space d, ℂ) to itself which maps ψ to (‖x‖² + ε²)^(s/2) • ψ.

Equations

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

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

The radius operator to power s, regularized by ε ≠ 0, is the continuous linear map from 𝓢(Space d, ℂ) to itself which maps ψ to (‖x‖² + ε²)^(s/2) • ψ.

Equations

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

theorem QuantumMechanics.radiusRegPowOperator_apply_fun {d : ℕ} (ε : ℝˣ) (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) : ⇑(𝐫[ε,s] ψ) = fun (x : Space d) => (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • ψ x

@[simp]

theorem QuantumMechanics.radiusRegPowOperator_apply {d : ℕ} (ε : ℝˣ) (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) (x : Space d) : (𝐫[ε,s] ψ) x = (‖x‖ ^ 2 + ↑ε ^ 2) ^ (s / 2) • ψ x

@[simp]

theorem QuantumMechanics.radiusRegPowOperator_comp_eq {d : ℕ} (ε : ℝˣ) (s t : ℝ) : 𝐫[ε,s].comp 𝐫[ε,t] = 𝐫[ε,s + t]

@[simp]

theorem QuantumMechanics.radiusRegPowOperator_zero {d : ℕ} (ε : ℝˣ) : 𝐫[ε,0] = 1

theorem QuantumMechanics.positionOperatorSqr_eq (d : ℕ) (ε : ℝˣ) : ∑ i : Fin d, 𝐱[i].comp 𝐱[i] = 𝐫[ε,2] - ↑ε ^ 2 • 1

C. Unbounded position vector operator

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

The position operators defined on the Schwartz submodule.

Equations

• QuantumMechanics.positionOperatorSchwartz i = ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv ∘ₗ ↑𝐱[i] ∘ₗ ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv.symm

theorem QuantumMechanics.positionOperatorSchwartz_isSymmetric {d : ℕ} (i : Fin d) : (positionOperatorSchwartz i).IsSymmetric

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

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

Equations

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

D. Unbounded regularized radius operator

def QuantumMechanics.radiusRegPowOperatorSchwartz {d : ℕ} (ε : ℝˣ) (s : ℝ) : ↥(SpaceDHilbertSpace.schwartzSubmodule d) →ₗ[ℂ] ↥(SpaceDHilbertSpace.schwartzSubmodule d)

The (regularized) radius operators defined on the Schwartz submodule.

Equations

• QuantumMechanics.radiusRegPowOperatorSchwartz ε s = ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv ∘ₗ ↑𝐫[ε,s] ∘ₗ ↑QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv.symm

theorem QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric {d : ℕ} (ε : ℝˣ) (s : ℝ) : (radiusRegPowOperatorSchwartz ε s).IsSymmetric

def QuantumMechanics.radiusRegPowUnboundedOperator {d : ℕ} (ε : ℝˣ) (s : ℝ) : UnboundedOperator ↥(SpaceDHilbertSpace d) ↥(SpaceDHilbertSpace d)

The symmetric (regularized) radius unbounded operators with domain the Schwartz submodule of the Hilbert space.

Equations

• QuantumMechanics.radiusRegPowUnboundedOperator ε s = QuantumMechanics.UnboundedOperator.ofSymmetric ⋯ ⋯