Exchange covariance of one-particle insertion

The concrete insertion maps intertwine simultaneous exchange with the remaining-coordinate unitary. Pairing with an antisymmetric state then gives equality of contraction norms across particle coordinates.

theorem LiebThirring.simultaneousPermutation_oneParticleInsertion {N q : ℕ} (i j : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (v : ↥(RestState i q)) : simultaneousPermutation (Equiv.swap i j) ((oneParticleInsertion i f) v) = (oneParticleInsertion j f) ((restExchange i j) v)

Exchanging particles transports insertion into the exchanged coordinate.

theorem LiebThirring.oneParticleContraction_exchange {N q : ℕ} (i j : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (ψ : State N q) (hψ : antisymmetric ψ) (hij : i ≠ j) : (oneParticleContraction j f) ψ = -(restExchange i j) ((oneParticleContraction i f) ψ)

On an antisymmetric state, exchange identifies the contracted vectors up to sign and the remaining-coordinate unitary.

theorem LiebThirring.oneParticleContraction_norm_eq {N q : ℕ} (i j : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (ψ : State N q) (hψ : antisymmetric ψ) : ‖(oneParticleContraction j f) ψ‖ = ‖(oneParticleContraction i f) ψ‖

The concrete contraction norms agree across all particle coordinates.

theorem LiebThirring.oneParticleProjection_norm_eq {N q : ℕ} (i j : Fin N) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)) (hf : ‖f‖ = 1) (ψ : State N q) (hψ : antisymmetric ψ) : ‖(oneParticleProjection j f) ψ‖ = ‖(oneParticleProjection i f) ψ‖

Equality of unit-vector projection norms on an antisymmetric state.