Spatial particle configurations

Euclidean spatial configurations, coordinate insertion and particle permutations.

@[reducible]

def LiebThirring.Position : Type

Three-dimensional Euclidean physical space.

Equations

• LiebThirring.Position = EuclideanSpace ℝ (Fin 3)

@[reducible]

def LiebThirring.Configuration (N : ℕ) : Type

Euclidean spatial coordinates of all particles.

Equations

• LiebThirring.Configuration N = EuclideanSpace ℝ (Fin N × Fin 3)

def LiebThirring.particlePosition {N : ℕ} (x : Configuration N) (i : Fin N) : Position

The spatial position of the selected particle.

Equations

• LiebThirring.particlePosition x i = WithLp.toLp 2 fun (a : Fin 3) => x.ofLp (i, a)

def LiebThirring.permutePositions {N : ℕ} (σ : Equiv.Perm (Fin N)) (x : Configuration N) : Configuration N

Relabel the spatial coordinates by a permutation of the particles.

Equations

• LiebThirring.permutePositions σ x = WithLp.toLp 2 fun (ia : Fin N × Fin 3) => x.ofLp (σ ia.1, ia.2)

@[reducible]

def LiebThirring.OtherConfiguration {N : ℕ} (i : Fin N) : Type

Spatial coordinates of the particles other than the selected particle.

Equations

• LiebThirring.OtherConfiguration i = EuclideanSpace ℝ ({ j : Fin N // j ≠ i } × Fin 3)

def LiebThirring.insertParticle {N : ℕ} (i : Fin N) (x : Position) (y : OtherConfiguration i) : Configuration N

Fill the selected spatial coordinate while retaining all other particle coordinates.

Equations

• LiebThirring.insertParticle i x y = WithLp.toLp 2 fun (ja : Fin N × Fin 3) => if h : ja.1 = i then x.ofLp ja.2 else y.ofLp (⟨ja.1, h⟩, ja.2)