Almost-everywhere equality of particle marginals #
Particle marginals of an antisymmetric state agree as functions almost everywhere, strengthening the existing equality of marginal tests.
The density is the particle count times any selected marginal almost everywhere. Selecting i: Fin N already excludes the vacuum.
theorem
LiebThirring.particle_marginal_eq_ae
{N q : ℕ}
(ψ : State N q)
(hψ : antisymmetric ψ)
(i j : Fin N)
:
(fun (x : Position) => ∫⁻ (y : OtherConfiguration i), ↑‖↑↑ψ (insertParticle i x y)‖₊ ^ 2) =ᵐ[MeasureTheory.volume]
fun (x : Position) => ∫⁻ (y : OtherConfiguration j), ↑‖↑↑ψ (insertParticle j x y)‖₊ ^ 2
Particle marginals of an antisymmetric state agree as functions almost everywhere, strengthening the existing equality of marginal tests.
theorem
LiebThirring.density_eq_mul_particle_marginal_ae
{N q : ℕ}
(ψ : State N q)
(hψ : antisymmetric ψ)
(i : Fin N)
:
density ψ =ᵐ[MeasureTheory.volume] fun (x : Position) =>
↑N * ∫⁻ (y : OtherConfiguration i), ↑‖↑↑ψ (insertParticle i x y)‖₊ ^ 2
The density is the particle count times any selected marginal almost
everywhere. Selecting i: Fin N already excludes the vacuum.