One-body Coulomb control by Fourier kinetic energy

Squared Schwartz L² norm, in nonnegative extended-integral form.

Every L² state has its Coulomb expectation bounded by its mass plus four times its Fourier kinetic energy, uniformly in the pole.

theorem LiebThirring.lintegral_schwartz_norm_sq_eq_enorm_toLp_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : SchwartzMap Position E) : ∫⁻ (x : Position), ↑‖f x‖₊ ^ 2 = ‖f.toLp 2 MeasureTheory.volume‖ₑ ^ 2

Squared Schwartz L² norm, in nonnegative extended-integral form.

theorem LiebThirring.lintegral_coulomb_le_of_fourier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (c : Position) (u : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) : ∫⁻ (x : Position), coulombKernel x c * ↑‖↑↑u x‖₊ ^ 2 ≤ ↑‖u‖₊ ^ 2 + 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position E) u) ξ‖₊ ^ 2

Every L² state has its Coulomb expectation bounded by its mass plus four times its Fourier kinetic energy, uniformly in the pole.