d-dimensional quantum operators

Stream: PhysLean

[Gregory Loges]

Hi all. I think I've oriented myself and refreshed a bit with lean going through some of 'mathematics in lean'. Part of making it to my goal of hydrogen's O(4) symmetry will be generalizing the pre-existing one-dimensional quantum mechanics to d dimensions, building upon PhysLean Space(AndTime).

Before forging ahead I would love some feedback from those with more experience than me about some "design" choices. I can imagine a few definitions for the position (vector) operator, either as a whole or component-wise:

def positionOperator (ψ : Space d → ℂ) : Space d → EuclideanSpace ℂ (Fin d) :=
  fun x ↦ WithLp.toLp 2 (fun i ↦ x i * ψ x)

def positionOperator' : (Space d → ℂ) → (Space d → EuclideanSpace ℂ (Fin d)) :=
  fun ψ x ↦ WithLp.toLp 2 (fun i ↦ x i * ψ x)

def positionOperatorComponent (i : Fin d) : (Space d → ℂ) → (Space d → ℂ) := fun ψ x ↦ x i * ψ x

def positionOperatorComponent' (i : Fin d) (ψ : Space d → ℂ) : Space d → ℂ := fun x ↦ x i * ψ x

To my knowledge positionOperator and positionOperator' are functionally identically, but is there a reason to prefer having ψ explicit or not? Is it better to define the vector operator and have notation for extracting the i-th component, or just work directly with positionOperatorComponent(s)?
Similarly for momentum (vector) operator:

def momentumOperator (ψ : Space d → ℂ) : Space d → EuclideanSpace ℂ (Fin d) :=
  fun x ↦ WithLp.toLp 2 (fun i ↦ (- Complex.I * ℏ) • ∂[i] ψ x)

def momentumOperator' : (Space d → ℂ) → (Space d → EuclideanSpace ℂ (Fin d)) :=
  fun ψ x ↦ WithLp.toLp 2 (fun i ↦ (- Complex.I * ℏ) • ∂[i] ψ x)

def momentumOperatorComponent'' (i : Fin d) : (Space d → ℂ) → (Space d → ℂ) :=
  fun ψ x ↦ momentumOperator ψ x i

def momentumOperatorComponent (i : Fin d) : (Space d → ℂ) → (Space d → ℂ) :=
  (- Complex.I * ℏ) • ∂[i]

def momentumOperatorComponent' (i : Fin d) (ψ : Space d → ℂ) : Space d → ℂ :=
  (- Complex.I * ℏ) • ∂[i] ψ

[Joseph Tooby-Smith]

I think it would be better to work directly with positionOperatorComponent but I would define it directly as a linear map. There are some examples of similar operators in, for example:

https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/Operators/Position.lean

[Joseph Tooby-Smith]

I think positionOperatorComponent is better here, because really this should be happing the Hilbert space to itself, and here Space d → ℂ is the (approximation) of the Hilbert space.

[Gregory Loges]

Thanks, I've made some progress on these and have the definition

/-- Component `i` of the position operator is the continuous linear map
from `𝓢(Space d, ℂ)` to itself which maps `ψ` to `xᵢψ`. -/
@[sorryful]
def positionOperator {d : ℕ} (i : Fin d) : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ) := by
  refine mkCLM (fun ψ x ↦ ↑(x i) * ψ x) ?hadd ?hsmul ?hsmooth ?hbound

  etc.

nearly sorry-free, following the 1d proof of boundedness. Similarly for the momentum operators.

I'd like to make my first pull request with these before I get too far along. Is there anything special I need to keep in mind? I have already marked both definitions with @[sorryful].

[Moritz Doll]

The operators used in here are coordinate free versions of what you want: docs#SchwartzMap.fourier_fderivCLM_eq

[Joseph Tooby-Smith]

Nice @Gregory Loges ! I think having coordinate dependent versions like the one Gregory has written is a good thing (as it is what the physicist would naturally think off). But if we can connect them to coordinate independent versions, as per Moritz's message, (maybe at a later date) then even better.

Concerning making your first pull-request. The only thing you have to really worry about is whether the linters pass. These will run once you make your PR on GitHub, but you can run them locally with instructions here: https://github.com/HEPLean/PhysLean/blob/master/scripts/README.md.

[Gregory Loges]

Thanks for pointing these out, @Moritz Doll. I'm still getting used to deciphering and searching mathlib.
If I understand correctly, the momentum operator could be defined to be $-\mathrm{i}\hbar$ times docs#SchwartzMap.fderivCLM of type

𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, Space d →[ℝ] ℂ)

and the $i^\text{th}$ component could then be extracted by feeding Space.basis i into Space d →[ℝ] ℂ. I think using these if possible would be nice in order to take advantage of the pre-existing machinery; let me see if I can make this work!

I'll go ahead with a PR soon, since the definition of angular momentum components and some of the commutators I have worked out don't depend on these details.

[Moritz Doll]

It might be even easier using lineDerivOpCLM applied with Space.basis i. Then you don't have to fiddle around with docs#SchwartzMap.evalCLM