Compact Voronoi cell and exterior divergence formulas

Cell divergence theorem proved by coordinate line slicing.

Equation, with precisely the directed bisector measures used in the energy deficit.

theorem LiebThirring.integrable_compact_directional_derivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Position → E) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (v : Position) : MeasureTheory.Integrable (fun (x : Position) => (fderiv ℝ g x) v) MeasureTheory.volume

theorem LiebThirring.integral_compact_directional_derivative_eq_zero (g : Position → ℝ) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : Fin 3) : ∫ (x : Position), (fderiv ℝ g x) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) = 0

theorem LiebThirring.fderiv_position_component (V : Position → Position) (hV : ContDiff ℝ 1 V) (a : Fin 3) (x v : Position) : (fderiv ℝ (fun (y : Position) => (V y).ofLp a) x) v = ((fderiv ℝ V x) v).ofLp a

theorem LiebThirring.integrable_positionDivergence (V : Position → Position) (hV : ContDiff ℝ 1 V) (hVc : HasCompactSupport V) : MeasureTheory.Integrable (positionDivergence V) MeasureTheory.volume

theorem LiebThirring.integral_positionDivergence_eq_zero (V : Position → Position) (hV : ContDiff ℝ 1 V) (hVc : HasCompactSupport V) : ∫ (x : Position), positionDivergence V x = 0

theorem LiebThirring.voronoiCell_compact_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (V : Position → Position) (hV : ContDiff ℝ 1 V) (hVc : HasCompactSupport V) : ∫ (x : Position) in voronoiCell R k, positionDivergence V x = ∑ l : { l : Fin M // l ≠ k }, ∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯

Cell divergence theorem proved by coordinate line slicing.

theorem LiebThirring.voronoiExterior_compact_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (V : Position → Position) (hV : ContDiff ℝ 1 V) (hVc : HasCompactSupport V) : ∫ (x : Position) in (voronoiCell R k)ᶜ, positionDivergence V x = -∑ l : { l : Fin M // l ≠ k }, ∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯

Equation, with precisely the directed bisector measures used in the energy deficit.