Spin-valued quantum states

The spin and L² carriers are separated from spatial geometry so that electrostatic modules do not import Fourier theory merely to use positions and configurations.

@[reducible]

def LiebThirring.SpinLabels (N q : ℕ) : Type

Assignments of one of the available spin labels to each particle.

Equations

• LiebThirring.SpinLabels N q = (Fin N → Fin q)

@[reducible]

def LiebThirring.SpinAmplitudes (N q : ℕ) : Type

Complex amplitudes for every spin assignment, with the Euclidean norm.

Equations

• LiebThirring.SpinAmplitudes N q = EuclideanSpace ℂ (LiebThirring.SpinLabels N q)

@[reducible]

def LiebThirring.State (N q : ℕ) : Type

Square-integrable spin-valued wavefunctions on the spatial configuration space.

Equations

• LiebThirring.State N q = ↥(MeasureTheory.Lp (LiebThirring.SpinAmplitudes N q) 2 MeasureTheory.volume)

def LiebThirring.permuteSpins {N q : ℕ} (σ : Equiv.Perm (Fin N)) (s : SpinLabels N q) : SpinLabels N q

Relabel spin assignments by the same particle permutation.

Equations

• LiebThirring.permuteSpins σ s i = s (σ i)