Directional integration over a Voronoi cell

Fubini and the planar projection formula turn the almost-everywhere scalar line identity into the cell integration-by-parts formula.

theorem LiebThirring.integrable_compact_bisectorSurfaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (g : Position → ℝ) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable g (bisectorSurfaceMeasure R hR k l hkl)

theorem LiebThirring.integrable_coordinateFaceTerm {M : ℕ} (R : Fin M → Position) (k l : Fin M) (a : Fin 3) (g : Position → ℝ) (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (coordinateFaceTerm R k l a g) MeasureTheory.volume

theorem LiebThirring.integral_coordinateFaceTerm {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (a : Fin 3) (g : Position → ℝ) : ∫ (q : Planar), coordinateFaceTerm R k l a g q = (bisectorNormal R k l).ofLp a * ∫ (x : Position) in voronoiFace R k l, g x ∂bisectorSurfaceMeasure R hR k l hkl

theorem LiebThirring.voronoiCell_compact_directional_integral {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (a : Fin 3) (g : Position → ℝ) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) : ∫ (x : Position) in voronoiCell R k, (fderiv ℝ g x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) = ∑ l : { l : Fin M // l ≠ k }, (bisectorNormal R k ↑l).ofLp a * ∫ (x : Position) in voronoiFace R k ↑l, g x ∂bisectorSurfaceMeasure R hR k ↑l ⋯