Measurability, testing and mass of the one-particle density

Arbitrary representatives agreeing almost everywhere give the same density almost everywhere, with no measurability assumption on the replacement.

theorem LiebThirring.measurable_particlePosition {N : ℕ} (i : Fin N) : Measurable fun (x : Configuration N) => particlePosition x i

theorem LiebThirring.measurable_state_norm_sq {N q : ℕ} (ψ : State N q) : Measurable fun (x : Configuration N) => ↑‖↑↑ψ x‖₊ ^ 2

theorem LiebThirring.measurable_inserted_state_norm_sq {N q : ℕ} (ψ : State N q) (i : Fin N) : Measurable fun (z : Position × OtherConfiguration i) => ↑‖↑↑ψ (insertParticle i z.1 z.2)‖₊ ^ 2

theorem LiebThirring.measurable_particle_marginal {N q : ℕ} (ψ : State N q) (i : Fin N) : Measurable fun (x : Position) => ∫⁻ (y : OtherConfiguration i), ↑‖↑↑ψ (insertParticle i x y)‖₊ ^ 2

theorem LiebThirring.measurable_density {N q : ℕ} (ψ : State N q) : Measurable (density ψ)

theorem LiebThirring.particle_marginal_testing {N q : ℕ} (ψ : State N q) (i : Fin N) (v : Position → ENNReal) (hv : Measurable v) : ∫⁻ (x : Position), v x * ∫⁻ (y : OtherConfiguration i), ↑‖↑↑ψ (insertParticle i x y)‖₊ ^ 2 = ∫⁻ (x : Configuration N), v (particlePosition x i) * ↑‖↑↑ψ x‖₊ ^ 2

theorem LiebThirring.density_testing (N q : ℕ) (ψ : State N q) (v : Position → ENNReal) (hv : Measurable v) : ∫⁻ (x : Position), v x * density ψ x = ∑ i : Fin N, ∫⁻ (x : Configuration N), v (particlePosition x i) * ↑‖↑↑ψ x‖₊ ^ 2

theorem LiebThirring.lintegral_state_norm_sq {N q : ℕ} (ψ : State N q) : ∫⁻ (x : Configuration N), ↑‖↑↑ψ x‖₊ ^ 2 = ↑‖ψ‖₊ ^ 2

theorem LiebThirring.density_mass {N q : ℕ} (ψ : State N q) : ∫⁻ (x : Position), density ψ x = ↑N * ↑‖ψ‖₊ ^ 2