The derivative jump between adjacent screened representatives

The jump of directional derivatives across a genuine Voronoi face.

theorem LiebThirring.screenedCellPotential_sub {M : ℕ} (Z : NNReal) (R : Fin M → Position) (k l : Fin M) (x : Position) : screenedCellPotential Z R l x - screenedCellPotential Z R k x = ↑Z * ‖x - R k‖⁻¹ - ↑Z * ‖x - R l‖⁻¹

theorem LiebThirring.fderiv_screenedCellPotential_jump {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) {x : Position} (hx : x ∈ voronoiFace R k l) (v : Position) : (fderiv ℝ (screenedCellPotential Z R l) x) v - (fderiv ℝ (screenedCellPotential Z R k) x) v = -↑Z * ‖R l - R k‖ / ‖x - R k‖ ^ 3 * inner ℝ (bisectorNormal R k l) v