Off-pole Coulomb differentiation

Inverse distance is smooth and harmonic away from its pole.

theorem LiebThirring.contDiffAt_inv_nuclear_distance (y x : Position) (hx : x ≠ y) (n : WithTop ℕ∞) : ContDiffAt ℝ n (fun (z : Position) => ‖z - y‖⁻¹) x

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

theorem LiebThirring.fderiv_nuclear_distance_sq_rpow (y x v : Position) (hx : x ≠ y) (p : ℝ) : (fderiv ℝ (fun (z : Position) => (‖z - y‖ ^ 2) ^ p) x) v = 2 * p * (‖x - y‖ ^ 2) ^ (p - 1) * inner ℝ (x - y) v

theorem LiebThirring.hessian_nuclear_distance_sq_rpow (y x v : Position) (hx : x ≠ y) (p : ℝ) : ((fderiv ℝ (fderiv ℝ fun (z : Position) => (‖z - y‖ ^ 2) ^ p) x) v) v = 4 * p * (p - 1) * (‖x - y‖ ^ 2) ^ (p - 2) * inner ℝ (x - y) v ^ 2 + 2 * p * (‖x - y‖ ^ 2) ^ (p - 1) * inner ℝ v v

theorem LiebThirring.fderiv_inv_nuclear_distance (y x v : Position) (hx : x ≠ y) : (fderiv ℝ (fun (z : Position) => ‖z - y‖⁻¹) x) v = -inner ℝ (x - y) v / ‖x - y‖ ^ 3

theorem LiebThirring.laplacian_inv_nuclear_distance (y x : Position) (hx : x ≠ y) : Laplacian.laplacian (fun (z : Position) => ‖z - y‖⁻¹) x = 0