Splitting a second particle from a remaining-coordinate carrier

These ordered encodings split particle j from the coordinates complementary to i, or particle i from those complementary to j, while using the same ordered pair-rest carrier in both cases.

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

Split the coordinate j from the spatial indices complementary to i.

Equations

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

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

Split the coordinate i from the spatial indices complementary to j.

Equations

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

def LiebThirring.insertOtherParticleLeft {N : ℕ} (i j : Fin N) (z : Position) (y : OtherPairConfiguration i j) : OtherConfiguration i

Insert particle j into the spatial coordinates complementary to i.

Equations

• LiebThirring.insertOtherParticleLeft i j z y = WithLp.toLp 2 fun (ka : { j : Fin N // j ≠ i } × Fin 3) => if h : ↑ka.1 = j then z.ofLp ka.2 else y.ofLp (⟨↑ka.1, ⋯⟩, ka.2)

def LiebThirring.insertOtherParticleRight {N : ℕ} (i j : Fin N) (x : Position) (y : OtherPairConfiguration i j) : OtherConfiguration j

Insert particle i into the spatial coordinates complementary to j.

Equations

• LiebThirring.insertOtherParticleRight i j x y = WithLp.toLp 2 fun (ka : { j_1 : Fin N // j_1 ≠ j } × Fin 3) => if h : ↑ka.1 = i then x.ofLp ka.2 else y.ofLp (⟨↑ka.1, ⋯⟩, ka.2)

def LiebThirring.insertOtherSpinLeft {N q : ℕ} (i j : Fin N) (r : Fin q) (t : OtherPairSpinLabels i j q) : OtherSpinLabels i q

Insert spin j into the labels complementary to i.

Equations

• LiebThirring.insertOtherSpinLeft i j r t k = if h : ↑k = j then r else t ⟨↑k, ⋯⟩

def LiebThirring.insertOtherSpinRight {N q : ℕ} (i j : Fin N) (s : Fin q) (t : OtherPairSpinLabels i j q) : OtherSpinLabels j q

Insert spin i into the labels complementary to j.

Equations

• LiebThirring.insertOtherSpinRight i j s t k = if h : ↑k = i then s else t ⟨↑k, ⋯⟩

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

Spatial insertion into RestState i as a measurable equivalence.

Equations

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

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

Spatial insertion into RestState j as a measurable equivalence.

Equations

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

theorem LiebThirring.restLeftInsertionMeasurableEquiv_apply {N : ℕ} (i j : Fin N) (hij : i ≠ j) (w : Position × OtherPairConfiguration i j) : (restLeftInsertionMeasurableEquiv i j hij) w = insertOtherParticleLeft i j w.1 w.2

theorem LiebThirring.restRightInsertionMeasurableEquiv_apply {N : ℕ} (i j : Fin N) (hij : i ≠ j) (w : Position × OtherPairConfiguration i j) : (restRightInsertionMeasurableEquiv i j hij) w = insertOtherParticleRight i j w.1 w.2

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

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

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

Split remaining spin labels in the left orientation.

Equations

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

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

Split remaining spin labels in the right orientation.

Equations

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

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

Split off the left selected spin from the remaining spin assignment.

Equations

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

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

Split off the right selected spin from the remaining spin assignment.

Equations

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

theorem LiebThirring.insertParticle_insertOtherParticleLeft {N : ℕ} (i j : Fin N) (x z : Position) (y : OtherPairConfiguration i j) : insertParticle i x (insertOtherParticleLeft i j z y) = insertParticlePair i j x z y

theorem LiebThirring.insertParticle_insertOtherParticleRight {N : ℕ} (i j : Fin N) (hij : i ≠ j) (x z : Position) (y : OtherPairConfiguration i j) : insertParticle j z (insertOtherParticleRight i j x y) = insertParticlePair i j x z y

theorem LiebThirring.insertSpin_insertOtherSpinLeft {N q : ℕ} (i j : Fin N) (s r : Fin q) (t : OtherPairSpinLabels i j q) : insertSpin i s (insertOtherSpinLeft i j r t) = insertSpinPair i j s r t

theorem LiebThirring.insertSpin_insertOtherSpinRight {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (s r : Fin q) (t : OtherPairSpinLabels i j q) : insertSpin j r (insertOtherSpinRight i j s t) = insertSpinPair i j s r t