Exchange of full Fourier energies

Fourier covariance gives equality of exchanged particle energies and the exchange-odd L² identity.

theorem LiebThirring.particleFourierEnergy_eq {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (i j : Fin N) : particleFourierEnergy ψ i = particleFourierEnergy ψ j

All full-space particle Fourier energies of an antisymmetric state agree.

theorem LiebThirring.kineticEnergy_eq_mul_particleFourierEnergy {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (i : Fin N) : kineticEnergy ψ = ↑N * particleFourierEnergy ψ i

The extended kinetic energy is the particle count times any selected full Fourier energy, including infinite energy.

theorem LiebThirring.simultaneousPermutation_swap_eq_neg {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (i j : Fin N) (hij : i ≠ j) : simultaneousPermutation (Equiv.swap i j) ψ = -ψ

A transposition of distinct particles acts by negation on an antisymmetric L² state. This is an equality of classes, not only of representative values.