Regularization of the Coulomb kernel

The regularized inverse-distance kernel of the fundamental solution.

The nonnegative approximate-identity density -Δ G_ε in the fundamental solution.

noncomputable def LiebThirring.regularizedCoulombKernel (ε : ℝ) (x : Position) : ℝ

The regularized inverse-distance kernel of the fundamental solution.

Equations

• LiebThirring.regularizedCoulombKernel ε x = (‖x‖ ^ 2 + ε ^ 2) ^ (-(1 / 2))

noncomputable def LiebThirring.coulombApproximationDensity (ε : ℝ) (x : Position) : ℝ

The nonnegative approximate-identity density -Δ G_ε in the fundamental solution.

Equations

• LiebThirring.coulombApproximationDensity ε x = 3 * ε ^ 2 * (‖x‖ ^ 2 + ε ^ 2) ^ (-(5 / 2))

theorem LiebThirring.norm_sq_add_sq_pos {ε : ℝ} (hε : 0 < ε) (x : Position) : 0 < ‖x‖ ^ 2 + ε ^ 2

The squared regularized distance is strictly positive.

theorem LiebThirring.contDiff_regularizedCoulombKernel {ε : ℝ} (hε : 0 < ε) : ContDiff ℝ (↑⊤) (regularizedCoulombKernel ε)

The regularized kernel is smooth everywhere for positive regularization scale.

theorem LiebThirring.fderiv_norm_sq_add_sq_rpow {ε : ℝ} (hε : 0 < ε) (p : ℝ) (x v : Position) : (fderiv ℝ (fun (z : Position) => (‖z‖ ^ 2 + ε ^ 2) ^ p) x) v = 2 * p * (‖x‖ ^ 2 + ε ^ 2) ^ (p - 1) * inner ℝ x v

First directional derivative of a regularized radial power.

theorem LiebThirring.hessian_norm_sq_add_sq_rpow {ε : ℝ} (hε : 0 < ε) (p : ℝ) (x v : Position) : ((fderiv ℝ (fderiv ℝ fun (z : Position) => (‖z‖ ^ 2 + ε ^ 2) ^ p) x) v) v = 4 * p * (p - 1) * (‖x‖ ^ 2 + ε ^ 2) ^ (p - 2) * inner ℝ x v ^ 2 + 2 * p * (‖x‖ ^ 2 + ε ^ 2) ^ (p - 1) * inner ℝ v v

The directional Hessian of a regularized radial power.

theorem LiebThirring.hessian_regularizedCoulombKernel {ε : ℝ} (hε : 0 < ε) (x v : Position) : ((fderiv ℝ (fderiv ℝ (regularizedCoulombKernel ε)) x) v) v = 3 * (‖x‖ ^ 2 + ε ^ 2) ^ (-(5 / 2)) * inner ℝ x v ^ 2 - (‖x‖ ^ 2 + ε ^ 2) ^ (-(3 / 2)) * inner ℝ v v

The directional Hessian of the regularized Coulomb kernel in the fundamental solution.

theorem LiebThirring.laplacian_regularizedCoulombKernel {ε : ℝ} (hε : 0 < ε) (x : Position) : Laplacian.laplacian (regularizedCoulombKernel ε) x = -coulombApproximationDensity ε x

The exact negative Laplacian of the regularized kernel, the fundamental solution.

theorem LiebThirring.coulombApproximationDensity_nonneg (ε : ℝ) (x : Position) : 0 ≤ coulombApproximationDensity ε x

The density in the regularization argument is nonnegative.

theorem LiebThirring.laplacian_regularizedCoulombKernel_sub {ε : ℝ} (hε : 0 < ε) (y x : Position) : Laplacian.laplacian (fun (z : Position) => regularizedCoulombKernel ε (z - y)) x = -coulombApproximationDensity ε (x - y)

Translation of the regularized Coulomb Laplacian to an arbitrary pole.

theorem LiebThirring.integral_regularizedCoulombKernel_sub_mul_laplacian {ε : ℝ} (hε : 0 < ε) {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (y : Position) : ∫ (x : Position), regularizedCoulombKernel ε (x - y) * Laplacian.laplacian f x = -∫ (x : Position), coulombApproximationDensity ε (x - y) * f x

the fundamental solution for a regularized kernel centered at an arbitrary pole.