Coordinate norms and singled-out spin encoding

The configuration norm is the sum of particle squared norms (coordinate norms).

The amplitude norm is the sum of squared scalar spin amplitudes (coordinate norms).

@[reducible, inline]

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

Spins of all particles other than the selected particle.

Equations

• LiebThirring.OtherSpinLabels i q = ({ j : Fin N // j ≠ i } → Fin q)

def LiebThirring.insertSpin {N q : ℕ} (i : Fin N) (s : Fin q) (t : OtherSpinLabels i q) : SpinLabels N q

Insert the selected spin into a configuration of the remaining spins.

Equations

• LiebThirring.insertSpin i s t j = if h : j = i then s else t ⟨j, h⟩

@[simp]

theorem LiebThirring.insertSpin_self {N q : ℕ} (i : Fin N) (s : Fin q) (t : OtherSpinLabels i q) : insertSpin i s t i = s

@[simp]

theorem LiebThirring.insertSpin_other {N q : ℕ} (i : Fin N) (s : Fin q) (t : OtherSpinLabels i q) (j : { j : Fin N // j ≠ i }) : insertSpin i s t ↑j = t j

def LiebThirring.spinInsertionEquiv {N q : ℕ} (i : Fin N) : Fin q × OtherSpinLabels i q ≃ SpinLabels N q

Split a spin assignment into the selected spin and the remaining spins.

Equations

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

noncomputable def LiebThirring.spinCurryingLinearIsometryEquiv {N q : ℕ} (i : Fin N) : SpinAmplitudes N q ≃ₗᵢ[ℂ] PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherSpinLabels i q)

Spin regrouping as a complex linear isometry, before spatial currying.

Equations

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

@[simp]

theorem LiebThirring.spinCurryingLinearIsometryEquiv_apply {N q : ℕ} (i : Fin N) (u : SpinAmplitudes N q) (s : Fin q) (t : OtherSpinLabels i q) : (((spinCurryingLinearIsometryEquiv i) u).ofLp s).ofLp t = u.ofLp (insertSpin i s t)