Hardy and Coulomb bounds for Schwartz functions

Hardy on the Schwartz core after removing the regularization by Fatou.

The elementary comparison between the Coulomb and inverse-square kernels.

theorem LiebThirring.lintegral_coulomb_sq_schwartz_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : Position) (f : SchwartzMap Position E) : ∫⁻ (x : Position), coulombKernel x c ^ 2 * ↑‖f x‖₊ ^ 2 ≤ ENNReal.ofReal (4 * ∑ i : Fin 3, ∫ (x : Position), ‖(fderiv ℝ (⇑f) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) i)‖ ^ 2)

Hardy on the Schwartz core after removing the regularization by Fatou.

theorem LiebThirring.coulombKernel_le_one_add_sq (x c : Position) : coulombKernel x c ≤ 1 + coulombKernel x c ^ 2

The elementary comparison between the Coulomb and inverse-square kernels.

theorem LiebThirring.schwartz_dirichlet_eq_fourier {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap Position H) : ENNReal.ofReal (4 * ∑ i : Fin 3, ∫ (x : Position), ‖(fderiv ℝ (⇑f) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) i)‖ ^ 2) = 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖(FourierTransform.fourier f) ξ‖₊ ^ 2

The three coordinate derivative energies equal the radial Fourier kinetic integral.

theorem LiebThirring.lintegral_coulomb_sq_schwartz_fourier_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : Position) (f : SchwartzMap Position H) : ∫⁻ (x : Position), coulombKernel x c ^ 2 * ↑‖f x‖₊ ^ 2 ≤ 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖(FourierTransform.fourier f) ξ‖₊ ^ 2

Schwartz Hardy with the exact Mathlib Fourier normalization.

theorem LiebThirring.lintegral_coulomb_schwartz_fourier_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : Position) (f : SchwartzMap Position H) : ∫⁻ (x : Position), coulombKernel x c * ↑‖f x‖₊ ^ 2 ≤ (∫⁻ (x : Position), ↑‖f x‖₊ ^ 2) + 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖(FourierTransform.fourier f) ξ‖₊ ^ 2

The Schwartz Coulomb expectation is bounded by mass plus four kinetic energies.