The screened Green identity in each cell

The globally smooth extension agrees with the Coulomb representative near its closed cell. Green's second identity therefore applies without any singular field or unproved trace assumption.

noncomputable def LiebThirring.screenedCellBoundaryTerm {M : ℕ} (Z : NNReal) (R : Fin M → Position) (k l : Fin M) (f : Position → ℝ) (x : Position) : ℝ

The screened-potential boundary contribution of a Voronoi cell in Green’s identity.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.sum_slicingGreenComponent (g f : Position → ℝ) (n x : Position) : ∑ a : Fin 3, n.ofLp a * slicingGreenComponent g f a x = g x * (fderiv ℝ f x) n - f x * (fderiv ℝ g x) n

theorem LiebThirring.integrableOn_screenedCellBoundaryTerm {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (f : Position → ℝ) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : MeasureTheory.IntegrableOn (screenedCellBoundaryTerm Z R k l f) (voronoiFace R k l) (bisectorSurfaceMeasure R hR k l hkl)

theorem LiebThirring.integral_screenedPotentialReal_laplacian_voronoiCell {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (f : Position → ℝ) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position) in voronoiCell R k, screenedPotentialReal Z R x * Laplacian.laplacian f x = ∑ l : { l : Fin M // l ≠ k }, ∫ (x : Position) in voronoiFace R k ↑l, screenedCellBoundaryTerm Z R k (↑l) f x ∂bisectorSurfaceMeasure R hR k ↑l ⋯

The harmonic bulk term vanishes; only the directed screened face term remains.