Vacuum density-power integral

The density is zero everywhere in the vacuum.

The vacuum density-power integral vanishes for every positive real exponent.

theorem LiebThirring.density_vacuum {q : ℕ} (ψ : State 0 q) (x : Position) : density ψ x = 0

The density is zero everywhere in the vacuum.

theorem LiebThirring.lintegral_density_rpow_vacuum {q : ℕ} (ψ : State 0 q) (p : ℝ) (hp : 0 < p) : ∫⁻ (x : Position), density ψ x ^ p = 0

The vacuum density-power integral vanishes for every positive real exponent.