Particle Fourier energies

The Fourier kinetic energy associated with particle i (Fourier factorization).

Full kinetic energy is the sum of the particle energies, including at infinity.

noncomputable def LiebThirring.particleFourierEnergy {N q : ℕ} (ψ : State N q) (i : Fin N) : ENNReal

The Fourier kinetic energy associated with particle i (Fourier factorization).

Equations

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

theorem LiebThirring.kineticEnergy_eq_sum_particleFourierEnergy {N q : ℕ} (ψ : State N q) : kineticEnergy ψ = ∑ i : Fin N, particleFourierEnergy ψ i

Full kinetic energy is the sum of the particle energies, including at infinity.

noncomputable def LiebThirring.statePermutationLinearIsometryEquiv {N q : ℕ} (σ : Equiv.Perm (Fin N)) : State N q ≃ₗᵢ[ℂ] State N q

Simultaneous particle permutation packaged as a unitary on State.

Equations

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

noncomputable def LiebThirring.simultaneousPermutation {N q : ℕ} (σ : Equiv.Perm (Fin N)) (ψ : State N q) : State N q

The L² simultaneous spatial and spin permutation from the formulas.

Equations

• LiebThirring.simultaneousPermutation σ ψ = (LiebThirring.statePermutationLinearIsometryEquiv σ) ψ

@[simp]

theorem LiebThirring.statePermutationLinearIsometryEquiv_apply {N q : ℕ} (σ : Equiv.Perm (Fin N)) (ψ : State N q) : (statePermutationLinearIsometryEquiv σ) ψ = simultaneousPermutation σ ψ

theorem LiebThirring.simultaneousPermutation_apply_ae {N q : ℕ} (σ : Equiv.Perm (Fin N)) (ψ : State N q) : ∀ᵐ (x : Configuration N), ∀ (s : SpinLabels N q), (↑↑(simultaneousPermutation σ ψ) x).ofLp s = (↑↑ψ (permutePositions σ x)).ofLp (permuteSpins σ s)

The permutation operator has exactly the simultaneous representative.

theorem LiebThirring.fourier_simultaneousPermutation {N q : ℕ} (σ : Equiv.Perm (Fin N)) (ψ : State N q) : FourierTransform.fourier (simultaneousPermutation σ ψ) = simultaneousPermutation σ (FourierTransform.fourier ψ)

The full L² Fourier transform intertwines every simultaneous particle permutation.

theorem LiebThirring.simultaneousPermutation_eq_sign_smul {N q : ℕ} (σ : Equiv.Perm (Fin N)) (ψ : State N q) (hψ : antisymmetric ψ) : simultaneousPermutation σ ψ = ↑↑(Equiv.Perm.sign σ) • ψ

An antisymmetric state is an eigenvector of each simultaneous permutation.

theorem LiebThirring.antisymmetric_fourier {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) : antisymmetric (FourierTransform.fourier ψ)

Full Fourier transformation preserves the antisymmetry condition.