Two-particle insertion on the state carrier

Insert the same one-particle vector in two distinct coordinates.

The two-particle insertion has its literal nested product representative.

noncomputable def LiebThirring.doubleParticleInsertion {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) : PairRestState i j q →L[ℂ] State N q

Insert the same one-particle vector in two distinct coordinates.

Equations

• LiebThirring.doubleParticleInsertion i j hij f = ↑↑(LiebThirring.pairCurryingLinearIsometryEquiv i j hij).symm ∘SL LiebThirring.doubleFactorInsertion f

theorem LiebThirring.doubleParticleInsertion_apply_ae {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : PairRestState i j q) : ∀ᵐ (x : Position), ∀ (s : Fin q), ∀ᵐ (z : Position), ∀ (r : Fin q), ∀ᵐ (y : OtherPairConfiguration i j), ∀ (t : OtherPairSpinLabels i j q), (↑↑((doubleParticleInsertion i j hij f) v) (insertParticlePair i j x z y)).ofLp (insertSpinPair i j s r t) = (↑↑f x).ofLp s * (↑↑f z).ofLp r * (↑↑v y).ofLp t

The two-particle insertion has its literal nested product representative.

theorem LiebThirring.simultaneousPermutation_doubleParticleInsertion {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : PairRestState i j q) : simultaneousPermutation (Equiv.swap i j) ((doubleParticleInsertion i j hij f) v) = (doubleParticleInsertion i j hij f) v

Exchanging the two inserted coordinates fixes the double insertion.