Dominated convergence to the singular Coulomb kernel

The negative half-power of a squared norm is the real inverse norm.

The regularized kernel is bounded by the inverse norm away from the pole.

theorem LiebThirring.norm_sq_rpow_neg_half (x : Position) : (‖x‖ ^ 2) ^ (-(1 / 2)) = ‖x‖⁻¹

The negative half-power of a squared norm is the real inverse norm.

theorem LiebThirring.regularizedCoulombKernel_le_inv_norm (ε : ℝ) {x : Position} (hx : x ≠ 0) : regularizedCoulombKernel ε x ≤ ‖x‖⁻¹

The regularized kernel is bounded by the inverse norm away from the pole.

theorem LiebThirring.tendsto_regularizedCoulombKernel {x : Position} (hx : x ≠ 0) : Filter.Tendsto (fun (ε : ℝ) => regularizedCoulombKernel ε x) (nhdsWithin 0 (Set.Ioi 0)) (nhds ‖x‖⁻¹)

The regularized kernel tends pointwise to the inverse norm away from its pole.

theorem LiebThirring.tendsto_integral_regularizedCoulombKernel_sub_mul_laplacian {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : Position), regularizedCoulombKernel ε (x - y) * Laplacian.laplacian f x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : Position), ‖x - y‖⁻¹ * Laplacian.laplacian f x))

Dominated convergence for the regularized test-function pairing in the fundamental solution.