Density lower bounds for high Fourier fields

The positive part of a norm difference is bounded by the difference norm.

A quadratic low-field bound gives the corresponding square-root bound.

theorem LiebThirring.max_norm_sub_norm_le_norm_sub {H : Type u_1} [NormedAddCommGroup H] (a b : H) : max (‖a‖ - ‖b‖) 0 ≤ ‖a - b‖

The positive part of a norm difference is bounded by the difference norm.

theorem LiebThirring.norm_le_sqrt_mul_rpow_of_norm_sq_le {H : Type u_1} [NormedAddCommGroup H] (u : H) (C E : ℝ) (hC : 0 ≤ C) (hE : 0 ≤ E) (hu : ‖u‖ ^ 2 ≤ C * E ^ (3 / 2)) : ‖u‖ ≤ √C * E ^ (3 / 4)

A quadratic low-field bound gives the corresponding square-root bound.

theorem LiebThirring.densityField_density_data_ae {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : ∀ᵐ (x : Position), density ψ x ≠ ⊤ ∧ (density ψ x).toReal = ‖↑↑(densityField i ψ) x‖ ^ 2 ∧ √(density ψ x).toReal = ‖↑↑(densityField i ψ) x‖

Density finiteness and its real norm identification hold on one conull set.

theorem LiebThirring.densityField_high_bound_ae_of_lowMomentumBound {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) (hLow : ∀ (E : ℝ), 0 ≤ E → ∀ (x : Position), ‖lowFourierField (densityField i ψ) E x‖ ^ 2 ≤ ↑q * (1 / (6 * Real.pi ^ 2)) * E ^ (3 / 2)) : ∀ᵐ (x : Position), ∀ (E : ℝ), 0 ≤ E → max (√(density ψ x).toReal - √(↑q * (1 / (6 * Real.pi ^ 2))) * E ^ (3 / 4)) 0 ≤ ‖highFourierField (densityField i ψ) E x‖

the layer cake reverse triangle bound on a single density-conull set for every energy, assembled conditionally from the exact pointwise the low-momentum bound low-field estimate.