Currying a second particle from a remaining state #
The two equivalences here identify either one-particle remaining carrier with the same ordered second-factor space used by pair currying.
@[reducible, inline]
The second one-particle factor over the ordered pair-rest state.
Equations
- LiebThirring.RestFactorState i j q = ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => LiebThirring.PairRestState i j q) 2 MeasureTheory.volume)
Instances For
noncomputable def
LiebThirring.restCurryingLeftLinearIsometryEquiv
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
:
Split particle j from a state on the coordinates complementary to i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LiebThirring.restCurryingRightLinearIsometryEquiv
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
:
Split particle i from a state on the coordinates complementary to j,
using the same ordered pair-rest carrier as the left equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LiebThirring.restCurryingLeftLinearIsometryEquiv_apply_ae
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(v : ↥(RestState i q))
:
∀ᵐ (z : Position), ∀ (r : Fin q),
∀ᵐ (y : OtherPairConfiguration i j), ∀ (t : OtherPairSpinLabels i j q),
(↑↑((↑↑((restCurryingLeftLinearIsometryEquiv i j hij) v) z).ofLp r) y).ofLp t = (↑↑v (insertOtherParticleLeft i j z y)).ofLp (insertOtherSpinLeft i j r t)
Literal representative of left remaining-state currying.
theorem
LiebThirring.restCurryingRightLinearIsometryEquiv_apply_ae
{N q : ℕ}
(i j : Fin N)
(hij : i ≠ j)
(v : ↥(RestState j q))
:
∀ᵐ (x : Position), ∀ (s : Fin q),
∀ᵐ (y : OtherPairConfiguration i j), ∀ (t : OtherPairSpinLabels i j q),
(↑↑((↑↑((restCurryingRightLinearIsometryEquiv i j hij) v) x).ofLp s) y).ofLp t = (↑↑v (insertOtherParticleRight i j x y)).ofLp (insertOtherSpinRight i j s t)
Literal representative of right remaining-state currying.