The directional cell identity on almost every line

The compact scalar fundamental theorem, applied to each transverse line in a Voronoi cell. The resulting terms are oriented genuine-face values.

noncomputable def LiebThirring.coordinateFaceTerm {M : ℕ} (R : Fin M → Position) (k l : Fin M) (a : Fin 3) (g : Position → ℝ) (q : Planar) : ℝ

Boundary value selected by a coordinate slice of a genuine Voronoi face.

Equations

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

theorem LiebThirring.hasDerivAt_comp_coordinateLine (g : Position → ℝ) (hg : ContDiff ℝ 1 g) (a : Fin 3) (q : Planar) (t : ℝ) : HasDerivAt (fun (s : ℝ) => g (coordinateLine a q s)) ((fderiv ℝ g (coordinateLine a q t)) ((EuclideanSpace.basisFun (Fin 3) ℝ) a)) t

theorem LiebThirring.integral_coordinateLine_voronoiCell {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (a : Fin 3) (q : Planar) (hq : q ∉ slicingExceptionalSet R a) (g : Position → ℝ) (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) : ∫ (t : ℝ) in {t : ℝ | coordinateLine a q t ∈ voronoiCell R k}, (fderiv ℝ g (coordinateLine a q t)) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) = ∑ l : { l : Fin M // l ≠ k }, coordinateFaceTerm R k (↑l) a g q