The directed Voronoi boundary formula

The outward normal Coulomb flux on a nuclear face.

The normal component equals the half separation on the literal bisector plane.

noncomputable def LiebThirring.nuclearFaceFlux {M : ℕ} (R : Fin M → Position) (k l : Fin M) (y : Position) : ℝ

The outward normal Coulomb flux on a nuclear face.

Equations

• LiebThirring.nuclearFaceFlux R k l y = inner ℝ (LiebThirring.bisectorNormal R k l) (y - R k) / ‖y - R k‖ ^ 3

theorem LiebThirring.nuclearFaceFlux_on_face {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} {y : Position} (hy : y ∈ voronoiFace R k l) : nuclearFaceFlux R k l y = nuclearHalfDistance R k l / ‖y - R k‖ ^ 3

The normal component equals the half separation on the literal bisector plane.

theorem LiebThirring.nuclearFaceFlux_comm_on_face {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} {y : Position} (hy : y ∈ voronoiFace R k l) : nuclearFaceFlux R k l y = nuclearFaceFlux R l k y

The normal flux is the same in the two face orientations.

theorem LiebThirring.bisectorSurfaceMeasure_comm {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : bisectorSurfaceMeasure R hR k l hkl = bisectorSurfaceMeasure R hR l k ⋯

Orientation does not change Euclidean surface measure on a bisector.

theorem LiebThirring.nuclearFaceDensity_eq_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (Z : ℝ) {k l : Fin M} {y : Position} (hy : y ∈ voronoiFace R k l) : nuclearFaceDensity R Z k l y = Z / (2 * Real.pi) * nuclearFaceFlux R k l y

The density is exactly the normal flux times Z/(2π) on the face.

theorem LiebThirring.lintegral_nuclearFaceMeasure_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (h : Position → ENNReal) (hh : Measurable h) : ∫⁻ (y : Position), h y ∂nuclearFaceMeasure R hR Z k l hkl = ENNReal.ofReal (Z / (2 * Real.pi)) * ∫⁻ (y : Position) in voronoiFace R k l, h y * ENNReal.ofReal (nuclearFaceFlux R k l y) ∂bisectorSurfaceMeasure R hR k l hkl

Nonnegative single-face integration in outward-normal form.

theorem LiebThirring.lintegral_nuclearFaceFlux_comm {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (h : Position → ENNReal) : ∫⁻ (y : Position) in voronoiFace R k l, h y * ENNReal.ofReal (nuclearFaceFlux R k l y) ∂bisectorSurfaceMeasure R hR k l hkl = ∫⁻ (y : Position) in voronoiFace R l k, h y * ENNReal.ofReal (nuclearFaceFlux R l k y) ∂bisectorSurfaceMeasure R hR l k ⋯

The flux integral is invariant under swapping the nuclei, in the extended setting.

theorem LiebThirring.face_coefficient_eq_two_directed (Z : ℝ) : Z / (2 * Real.pi) = Z / (4 * Real.pi) + Z / (4 * Real.pi)

The factor Z/(2π) splits into the two directed factors Z/(4π).

theorem LiebThirring.lintegral_voronoiFaceMeasure_directed {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (h : Position → ENNReal) (hh : Measurable h) : ∫⁻ (y : Position), h y ∂voronoiFaceMeasure R hR Z = ENNReal.ofReal (Z / (4 * Real.pi)) * ∑ k : Fin M, ∑ l : { l : Fin M // l ≠ k }, ∫⁻ (y : Position) in voronoiFace R k ↑l, h y * ENNReal.ofReal (inner ℝ (bisectorNormal R k ↑l) (y - R k) / ‖y - R k‖ ^ 3) ∂bisectorSurfaceMeasure R hR k ↑l ⋯

Equation (6.3) tested against any nonnegative Borel function.

theorem LiebThirring.voronoiFaceDensity_lt_top {M : ℕ} (R : Fin M → Position) (Z : ℝ) (k l : Fin M) (y : Position) : voronoiFaceDensity R Z k l y < ⊤

Every face density is finite, including its zero extension.

theorem LiebThirring.integral_nuclearFaceMeasure_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (h : Position → ℝ) : ∫ (y : Position), h y ∂nuclearFaceMeasure R hR Z k l hkl = Z / (2 * Real.pi) * ∫ (y : Position) in voronoiFace R k l, h y * nuclearFaceFlux R k l y ∂bisectorSurfaceMeasure R hR k l hkl

A real face-charge integral is the weighted real surface integral, without a separate global measurability premise on the function.