Intertwining concrete coordinate insertion with pair factors

Pair currying sends insertion in the first or second selected particle to the corresponding abstract tensor-factor insertion.

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

Reassociate ordered pair coordinates so that insertion in coordinate j is expressed in its native one-particle splitting.

Equations

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

theorem LiebThirring.pairToRightRestMeasurableEquiv_apply {N : ℕ} (i j : Fin N) (hij : i ≠ j) (w : Position × Position × OtherPairConfiguration i j) : (pairToRightRestMeasurableEquiv i j hij) w = (w.2.1, insertOtherParticleRight i j w.1 w.2.2)

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

theorem LiebThirring.pairCurrying_oneParticleInsertion_left {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState i q)) : (pairCurryingLinearIsometryEquiv i j hij) ((oneParticleInsertion i f) v) = (firstFactorInsertion f) ((restCurryingLeftLinearIsometryEquiv i j hij) v)

Pair currying transports concrete insertion in coordinate i to insertion in the first abstract tensor factor.

theorem LiebThirring.pairCurrying_oneParticleInsertion_right {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState j q)) : (pairCurryingLinearIsometryEquiv i j hij) ((oneParticleInsertion j f) v) = (secondFactorInsertion f) ((restCurryingRightLinearIsometryEquiv i j hij) v)

Pair currying transports concrete insertion in coordinate j to insertion in the second abstract tensor factor.