Two-particle coordinate encoding

The coordinate splitting used to compare rank-one lifts in two distinct particle coordinates. The order of the two displayed particles is retained; simultaneous exchange therefore acts by swapping those two entries and fixes the remaining configuration.

def LiebThirring.pairInsertionIndexEquiv {N : ℕ} (i j : Fin N) (hij : i ≠ j) : Fin N × Fin 3 ≃ Fin 3 ⊕ Fin 3 ⊕ { k : Fin N // k ≠ i ∧ k ≠ j } × Fin 3

Partition the full spatial index into two selected particles and all remaining coordinates.

Equations

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

@[reducible, inline]

abbrev LiebThirring.OtherPairConfiguration {N : ℕ} (i j : Fin N) : Type

Spatial coordinates other than two specified distinct particles.

Equations

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

@[reducible, inline]

abbrev LiebThirring.OtherPairSpinLabels {N : ℕ} (i j : Fin N) (q : ℕ) : Type

Spin labels other than two specified distinct particles.

Equations

• LiebThirring.OtherPairSpinLabels i j q = ({ k : Fin N // k ≠ i ∧ k ≠ j } → Fin q)

def LiebThirring.insertParticlePair {N : ℕ} (i j : Fin N) (x z : Position) (y : OtherPairConfiguration i j) : Configuration N

Insert two distinct spatial particle coordinates.

Equations

• LiebThirring.insertParticlePair i j x z y = WithLp.toLp 2 fun (ka : Fin N × Fin 3) => if hi : ka.1 = i then x.ofLp ka.2 else if hj : ka.1 = j then z.ofLp ka.2 else y.ofLp (⟨ka.1, ⋯⟩, ka.2)

def LiebThirring.insertSpinPair {N q : ℕ} (i j : Fin N) (s r : Fin q) (t : OtherPairSpinLabels i j q) : SpinLabels N q

Insert two distinct spin coordinates.

Equations

• LiebThirring.insertSpinPair i j s r t k = if hi : k = i then s else if hj : k = j then r else t ⟨k, ⋯⟩

noncomputable def LiebThirring.pairInsertionMeasurableEquiv {N : ℕ} (i j : Fin N) (hij : i ≠ j) : Position × Position × OtherPairConfiguration i j ≃ᵐ Configuration N

The measurable coordinate equivalence associated with ordered insertion of two distinct particles.

Equations

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

theorem LiebThirring.pairInsertionMeasurableEquiv_apply {N : ℕ} (i j : Fin N) (hij : i ≠ j) (z : Position × Position × OtherPairConfiguration i j) : (pairInsertionMeasurableEquiv i j hij) z = insertParticlePair i j z.1 z.2.1 z.2.2

theorem LiebThirring.measurePreserving_pairInsertion {N : ℕ} (i j : Fin N) (hij : i ≠ j) : MeasureTheory.MeasurePreserving (⇑(pairInsertionMeasurableEquiv i j hij)) MeasureTheory.volume MeasureTheory.volume

Ordered insertion of two distinct particles preserves product volume.

def LiebThirring.spinPairInsertionEquiv {N q : ℕ} (i j : Fin N) (hij : i ≠ j) : Fin q × Fin q × OtherPairSpinLabels i j q ≃ SpinLabels N q

Split a spin assignment into two selected labels and the remaining labels.

Equations

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

noncomputable def LiebThirring.spinPairCurryingLinearIsometryEquiv {N q : ℕ} (i j : Fin N) (hij : i ≠ j) : SpinAmplitudes N q ≃ₗᵢ[ℂ] PiLp 2 fun (x : Fin q) => PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)

Regroup finite spin amplitudes into two selected spin factors.

Equations

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

theorem LiebThirring.permutePositions_swap_insertParticlePair {N : ℕ} (i j : Fin N) (hij : i ≠ j) (x z : Position) (y : OtherPairConfiguration i j) : permutePositions (Equiv.swap i j) (insertParticlePair i j x z y) = insertParticlePair i j z x y

Swapping the two displayed spatial entries is simultaneous particle exchange.

theorem LiebThirring.permuteSpins_swap_insertSpinPair {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (s r : Fin q) (t : OtherPairSpinLabels i j q) : permuteSpins (Equiv.swap i j) (insertSpinPair i j s r t) = insertSpinPair i j r s t

Swapping the two displayed spin entries is simultaneous particle exchange.