Currying on the state carriers

The one-particle currying isometry on the spatial and spin carriers.

The full currying complex linear isometric equivalence, with the original state as its source and the literal one-particle fiber as its target.

noncomputable def LiebThirring.oneParticleCurryingLinearIsometryEquiv {N q : ℕ} (i : Fin N) : State N q ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp (OneParticleFiber i q) 2 MeasureTheory.volume)

The full currying complex linear isometric equivalence, with the original state as its source and the literal one-particle fiber as its target.

Equations

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

noncomputable def LiebThirring.oneParticleCurrying {N q : ℕ} (i : Fin N) : State N q →ₗᵢ[ℂ] ↥(MeasureTheory.Lp (OneParticleFiber i q) 2 MeasureTheory.volume)

The one-particle currying isometry on the spatial and spin carriers.

Equations

• LiebThirring.oneParticleCurrying i = (LiebThirring.oneParticleCurryingLinearIsometryEquiv i).toLinearIsometry

theorem LiebThirring.oneParticleCurrying_ae {N q : ℕ} (i : Fin N) (ψ : State N q) : ∀ᵐ (x : Position), ∀ (s : Fin q), ∀ᵐ (y : OtherConfiguration i), ∀ (t : OtherSpinLabels i q), (↑↑((↑↑((oneParticleCurrying i) ψ) x).ofLp s) y).ofLp t = (↑↑ψ (insertParticle i x y)).ofLp (insertSpin i s t)

The currying representative identity, on one common full-measure outer set.