Spaces and slice integrability for one-particle currying

The Hilbert space of the remaining spatial and spin coordinates (currying).

The singled-out spin components with values in the remaining-state space (currying).

@[reducible, inline]

noncomputable abbrev LiebThirring.RestState {N : ℕ} (i : Fin N) (q : ℕ) : AddSubgroup (OtherConfiguration i →ₘ[MeasureTheory.volume] EuclideanSpace ℂ (OtherSpinLabels i q))

The Hilbert space of the remaining spatial and spin coordinates (currying).

Equations

• LiebThirring.RestState i q = MeasureTheory.Lp (EuclideanSpace ℂ (LiebThirring.OtherSpinLabels i q)) 2 MeasureTheory.volume

@[reducible, inline]

abbrev LiebThirring.OneParticleFiber {N : ℕ} (i : Fin N) (q : ℕ) : Type

The singled-out spin components with values in the remaining-state space (currying).

Equations

• LiebThirring.OneParticleFiber i q = PiLp 2 fun (x : Fin q) => ↥(LiebThirring.RestState i q)