Particle insertion and product volume

Partition spatial coordinates into particle i and the other particles.

Coordinate insertion as an equivalence of measurable spaces.

def LiebThirring.insertionIndexEquiv {N : ℕ} (i : Fin N) : Fin N × Fin 3 ≃ Fin 3 ⊕ { j : Fin N // j ≠ i } × Fin 3

Partition spatial coordinates into particle i and the other particles.

Equations

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

noncomputable def LiebThirring.insertionMeasurableEquiv {N : ℕ} (i : Fin N) : Position × OtherConfiguration i ≃ᵐ Configuration N

Coordinate insertion as an equivalence of measurable spaces.

Equations

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

theorem LiebThirring.insertionMeasurableEquiv_apply {N : ℕ} (i : Fin N) (z : Position × OtherConfiguration i) : (insertionMeasurableEquiv i) z = insertParticle i z.1 z.2

theorem LiebThirring.measurePreserving_insertion {N : ℕ} (i : Fin N) : MeasureTheory.MeasurePreserving (⇑(insertionMeasurableEquiv i)) MeasureTheory.volume MeasureTheory.volume

theorem LiebThirring.measurePreserving_insertParticle {N : ℕ} (i : Fin N) : MeasureTheory.MeasurePreserving (fun (z : Position × OtherConfiguration i) => insertParticle i z.1 z.2) MeasureTheory.volume MeasureTheory.volume

@[simp]

theorem LiebThirring.particlePosition_insertParticle {N : ℕ} (i : Fin N) (x : Position) (y : OtherConfiguration i) : particlePosition (insertParticle i x y) i = x