The curried density field

Curried fiber norms identify the particle marginals and the scaled density field.

theorem LiebThirring.piLp_enorm_sq {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E i)] (u : PiLp 2 E) : ‖u‖ₑ ^ 2 = ∑ i : ι, ‖u.ofLp i‖ₑ ^ 2

Extended squared norm of a finite Hilbert sum.

theorem LiebThirring.particle_marginal_eq_currying_norm_sq_ae {N q : ℕ} (i : Fin N) (ψ : State N q) : (fun (x : Position) => ∫⁻ (y : OtherConfiguration i), ↑‖↑↑ψ (insertParticle i x y)‖₊ ^ 2) =ᵐ[MeasureTheory.volume] fun (x : Position) => ↑‖↑↑((oneParticleCurrying i) ψ) x‖₊ ^ 2

Each marginal is the squared norm of the currying outer fiber a.e.

theorem LiebThirring.density_eq_mul_currying_norm_sq_ae {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : density ψ =ᵐ[MeasureTheory.volume] fun (x : Position) => ↑N * ↑‖↑↑((oneParticleCurrying i) ψ) x‖₊ ^ 2

The density is N times the squared norm of any selected curried fiber.

noncomputable def LiebThirring.densityField {N q : ℕ} (i : Fin N) (ψ : State N q) : ↥(MeasureTheory.Lp (OneParticleFiber i q) 2 MeasureTheory.volume)

The outer density field used by the Rumin argument.

Equations

• LiebThirring.densityField i ψ = ↑√↑N • (LiebThirring.oneParticleCurrying i) ψ

theorem LiebThirring.density_eq_densityField_norm_sq_ae {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : density ψ =ᵐ[MeasureTheory.volume] fun (x : Position) => ↑‖↑↑(densityField i ψ) x‖₊ ^ 2

The density is the squared fiber norm of the density field a.e.