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. Schwartz operators
  • A.1. Position vector
  • A.2. Radius powers (regularized)
  • A.3. Radius powers
    • A.3.1. As limit of regularized operators
• B. Unbounded operators
  • B.1. Position vector
  • B.2. Radius powers (regularized)

iv. References

A. Schwartz operators

A.1. Position vector

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] ψ) = (fun (x : Space d) => x.val i) • ⇑ψ

@[simp]

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

A.2. Radius powers (regularized)

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] = ContinuousLinearMap.id ℂ (SchwartzMap (Space d) ℂ)

theorem QuantumMechanics.positionOperatorSqr_eq {d : ℕ} (ε : ℝˣ) : ∑ i : Fin d, 𝐱[i].comp 𝐱[i] = 𝐫[ε,2] - ↑ε ^ 2 • ContinuousLinearMap.id ℂ (SchwartzMap (Space d) ℂ)

A.3. Radius powers

def QuantumMechanics.radiusPowOperator {d : ℕ} (s : ℝ) : SchwartzMap (Space d) ℂ →ₗ[ℂ] Space d → ℂ

The radius operator to power s is the linear map from 𝓢(Space d, ℂ) to Space d → ℂ that maps ψ to x ↦ ‖x‖ˢψ(x) (which is 'nearly' Schwartz for general s).

Equations

• 𝐫[s] = { toFun := fun (ψ : SchwartzMap (Space d) ℂ) => (fun (x : Space d) => ‖x‖ ^ s) • ⇑ψ, map_add' := ⋯, map_smul' := ⋯ }

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

The radius operator to power s is the linear map from 𝓢(Space d, ℂ) to Space d → ℂ that maps ψ to x ↦ ‖x‖ˢψ(x) (which is 'nearly' Schwartz for general s).

Equations

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

theorem QuantumMechanics.radiusPowOperator_apply_fun {d : ℕ} (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) : 𝐫[s] ψ = fun (x : Space d) => ‖x‖ ^ s • ψ x

@[simp]

theorem QuantumMechanics.radiusPowOperator_apply {d : ℕ} (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) (x : Space d) : 𝐫[s] ψ x = ‖x‖ ^ s • ψ x

theorem QuantumMechanics.radiusPowOperator_apply_contDiffAt {d : ℕ} (s : ℝ) (n : ℕ∞) (ψ : SchwartzMap (Space d) ℂ) {x : Space d} (hx : x ≠ 0) : ContDiffAt ℝ (↑n) (𝐫[s] ψ) x

x ↦ ‖x‖ˢψ(x) is smooth away from x = 0.

theorem QuantumMechanics.radiusPowOperator_apply_stronglyMeasurable {d : ℕ} (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) : MeasureTheory.StronglyMeasurable (𝐫[s] ψ)

x ↦ ‖x‖ˢψ(x) is strongly measurable.

theorem QuantumMechanics.radiusPowOperator_apply_memHS {d : ℕ} (s : ℝ) (h : 0 < ↑d + 2 * s) (ψ : SchwartzMap (Space d) ℂ) : SpaceDHilbertSpace.MemHS (𝐫[s] ψ)

x ↦ ‖x‖ˢψ(x) is square-integrable provided s is not too negative.

A.3.1. As limit of regularized operators

@[reducible, inline]

abbrev QuantumMechanics.nhdsZeroUnits : Filter ℝˣ

Neighborhoods of "0" in the non-zero reals, i.e. those sets containing (-ε,0) ∪ (0,ε) ⊆ ℝˣ for some ε > 0.

Equations

• QuantumMechanics.nhdsZeroUnits = Filter.comap (⇑(Units.coeHom ℝ)) (nhds 0)

instance QuantumMechanics.instNeBotUnitsRealNhdsZeroUnits : nhdsZeroUnits.NeBot

theorem QuantumMechanics.radiusRegPow_tendsto_radiusPow {d : ℕ} (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) {x : Space d} (hx : x ≠ 0) : Filter.Tendsto (fun (ε : ℝˣ) => (𝐫[ε,s] ψ) x) nhdsZeroUnits (nhds (𝐫[s] ψ x))

𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 except perhaps at x = 0.

theorem QuantumMechanics.radiusRegPow_tendsto_radiusPow' {d : ℕ} (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) (h : 0 ≤ s ∨ ψ 0 = 0) : Filter.Tendsto (fun (ε : ℝˣ) => ⇑(𝐫[ε,s] ψ)) nhdsZeroUnits (nhds (𝐫[s] ψ))

𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 provided 𝐫[ε,s] ψ 0 is bounded.

theorem QuantumMechanics.radiusRegPow_ae_tendsto_radiusPow {d : ℕ} (hd : 0 < d) (s : ℝ) (ψ : SchwartzMap (Space d) ℂ) : ∀ᵐ (x : Space d), Filter.Tendsto (fun (ε : ℝˣ) => (𝐫[ε,s] ψ) x) nhdsZeroUnits (nhds (𝐫[s] ψ x))

a.e. version of radiusRegPow_tendsto_radiusPow

theorem QuantumMechanics.radiusRegPow_ae_tendsto_iff {d : ℕ} (hd : 0 < d) {s : ℝ} {ψ : SchwartzMap (Space d) ℂ} {φ : Space d → ℂ} : (∀ᵐ (x : Space d), Filter.Tendsto (fun (ε : ℝˣ) => (𝐫[ε,s] ψ) x) nhdsZeroUnits (nhds (φ x))) ↔ φ =ᵐ[MeasureTheory.volume] 𝐫[s] ψ

B. Unbounded operators

B.1. Position vector

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 ⋯ ⋯

B.2. Radius powers (regularized)

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 ⋯ ⋯