Green's second identity on an open Voronoi cell

Compact tests eliminate outer boundary terms. The genuine-face terms follow from the directional cell identity proved by line slicing.

noncomputable def LiebThirring.slicingGreenComponent (g f : Position → ℝ) (a : Fin 3) (x : Position) : ℝ

A coordinate component of the vector field in Green’s identity.

Equations

• LiebThirring.slicingGreenComponent g f a x = g x * (fderiv ℝ f x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) - f x * (fderiv ℝ g x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)

theorem LiebThirring.contDiff_slicingGreenComponent {g f : Position → ℝ} (hg : ContDiff ℝ 2 g) (hf : ContDiff ℝ 2 f) (a : Fin 3) : ContDiff ℝ 1 (slicingGreenComponent g f a)

theorem LiebThirring.hasCompactSupport_slicingGreenComponent {g f : Position → ℝ} (hfc : HasCompactSupport f) (a : Fin 3) : HasCompactSupport (slicingGreenComponent g f a)

theorem LiebThirring.fderiv_slicingGreenComponent {g f : Position → ℝ} (hg : ContDiff ℝ 2 g) (hf : ContDiff ℝ 2 f) (a : Fin 3) (x : Position) : (fderiv ℝ (slicingGreenComponent g f a) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) = g x * ((fderiv ℝ (fderiv ℝ f) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) - f x * ((fderiv ℝ (fderiv ℝ g) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)

theorem LiebThirring.laplacian_green_eq_sum {g f : Position → ℝ} (hg : ContDiff ℝ 2 g) (hf : ContDiff ℝ 2 f) (x : Position) : g x * Laplacian.laplacian f x - f x * Laplacian.laplacian g x = ∑ a : Fin 3, (fderiv ℝ (slicingGreenComponent g f a) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)

theorem LiebThirring.voronoiCell_compact_green {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (g f : Position → ℝ) (hg : ContDiff ℝ 2 g) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position) in voronoiCell R k, g x * Laplacian.laplacian f x - f x * Laplacian.laplacian g x = ∑ l : { l : Fin M // l ≠ k }, ∫ (x : Position) in voronoiFace R k ↑l, ∑ a : Fin 3, (bisectorNormal R k ↑l).ofLp a * slicingGreenComponent g f a x ∂bisectorSurfaceMeasure R hR k ↑l ⋯

Green's second identity with explicit directed genuine-face integrals.