Particle permutations

Spatial coordinate permutation as a linear isometry.

The finite spin labels are permuted bijectively.

noncomputable def LiebThirring.permutationLinearIsometryEquiv {N : ℕ} (σ : Equiv.Perm (Fin N)) : Configuration N ≃ₗᵢ[ℝ] Configuration N

Spatial coordinate permutation as a linear isometry.

Equations

• LiebThirring.permutationLinearIsometryEquiv σ = LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ ((Equiv.symm σ).prodCongr (Equiv.refl (Fin 3)))

theorem LiebThirring.permutationLinearIsometryEquiv_apply {N : ℕ} (σ : Equiv.Perm (Fin N)) (x : Configuration N) : (permutationLinearIsometryEquiv σ) x = permutePositions σ x

theorem LiebThirring.measurePreserving_permutePositions {N : ℕ} (σ : Equiv.Perm (Fin N)) : MeasureTheory.MeasurePreserving (permutePositions σ) MeasureTheory.volume MeasureTheory.volume

theorem LiebThirring.measurableEmbedding_permutePositions {N : ℕ} (σ : Equiv.Perm (Fin N)) : MeasurableEmbedding (permutePositions σ)

@[simp]

theorem LiebThirring.particlePosition_permutePositions {N : ℕ} (σ : Equiv.Perm (Fin N)) (x : Configuration N) (i : Fin N) : particlePosition (permutePositions σ x) i = particlePosition x (σ i)

def LiebThirring.spinPermutationEquiv {N q : ℕ} (σ : Equiv.Perm (Fin N)) : SpinLabels N q ≃ SpinLabels N q

The finite spin labels are permuted bijectively.

Equations

• LiebThirring.spinPermutationEquiv σ = { toFun := LiebThirring.permuteSpins σ, invFun := LiebThirring.permuteSpins (Equiv.symm σ), left_inv := ⋯, right_inv := ⋯ }

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

Spin-coordinate reindexing is a complex linear isometry.

Equations

• LiebThirring.spinPermutationLinearIsometryEquiv σ = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (LiebThirring.spinPermutationEquiv σ).symm

theorem LiebThirring.norm_permutePositions_ae {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (σ : Equiv.Perm (Fin N)) : ∀ᵐ (x : Configuration N), ‖↑↑ψ (permutePositions σ x)‖ = ‖↑↑ψ x‖

theorem LiebThirring.nnnorm_permutePositions_ae {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (σ : Equiv.Perm (Fin N)) : ∀ᵐ (x : Configuration N), ‖↑↑ψ (permutePositions σ x)‖₊ = ‖↑↑ψ x‖₊

The norm equality also holds in the nonnegative norm used by the density.

theorem LiebThirring.particle_marginal_permutation {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (σ : Equiv.Perm (Fin N)) (i : Fin N) (v : Position → ENNReal) : ∫⁻ (x : Configuration N), v (particlePosition x (σ i)) * ↑‖↑↑ψ x‖₊ ^ 2 = ∫⁻ (x : Configuration N), v (particlePosition x i) * ↑‖↑↑ψ x‖₊ ^ 2

Relabeling particles preserves every nonnegative marginal test.

theorem LiebThirring.particle_marginals_eq {N q : ℕ} (ψ : State N q) (hψ : antisymmetric ψ) (i j : Fin N) (v : Position → ENNReal) : ∫⁻ (x : Configuration N), v (particlePosition x i) * ↑‖↑↑ψ x‖₊ ^ 2 = ∫⁻ (x : Configuration N), v (particlePosition x j) * ↑‖↑↑ψ x‖₊ ^ 2

All particle marginals of an antisymmetric state have the same tests.