One-particle density

The spatial density obtained by integrating out all other particle coordinates and summing over particles.

noncomputable def LiebThirring.density {N q : ℕ} (ψ : State N q) (x : Position) : ENNReal

One-particle density obtained by integrating out the remaining spatial coordinates.

Equations

• LiebThirring.density ψ x = ∑ i : Fin N, ∫⁻ (y : LiebThirring.OtherConfiguration i), ↑‖↑↑ψ (LiebThirring.insertParticle i x y)‖₊ ^ 2