Surface charge and coordinate graph integrals

Integration against one face charge, with the literal face charge density.

The literal unordered-face surface integral form of the ν.

theorem LiebThirring.integral_nuclearFaceMeasure_density {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (f : Position → ℝ) : ∫ (x : Position), f x ∂nuclearFaceMeasure R hR Z k l hkl = ∫ (x : Position) in voronoiFace R k l, nuclearFaceDensity R Z k l x * f x ∂bisectorSurfaceMeasure R hR k l hkl

Integration against one face charge, with the literal face charge density.

theorem LiebThirring.integral_voronoiFaceMeasure_density {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (f : Position → ℝ) (hf : MeasureTheory.Integrable f (voronoiFaceMeasure R hR Z)) : ∫ (x : Position), f x ∂voronoiFaceMeasure R hR Z = ∑ p : NuclearPair M, ∫ (x : Position) in voronoiFace R (↑p).1 (↑p).2, nuclearFaceDensity R Z (↑p).1 (↑p).2 x * f x ∂bisectorSurfaceMeasure R hR (↑p).1 (↑p).2 ⋯

The literal unordered-face surface integral form of the landed ν.

theorem LiebThirring.integrable_compact_voronoiFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) {f : Position → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) : MeasureTheory.Integrable f (voronoiFaceMeasure R hR Z)