Geometry for the positive Voronoi face measure

Half the separation of two nuclei, the height appearing in.

A frame chosen only to construct surface measure; its measure is independent of this choice, as established by bisectorSurfaceMeasure_eq.

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

Half the separation of two nuclei, the height appearing in (6.1).

Equations

• LiebThirring.nuclearHalfDistance R k l = ‖R l - R k‖ / 2

theorem LiebThirring.nuclearHalfDistance_pos {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : 0 < nuclearHalfDistance R k l

theorem LiebThirring.nuclearHalfDistance_comm {M : ℕ} (R : Fin M → Position) (k l : Fin M) : nuclearHalfDistance R k l = nuclearHalfDistance R l k

theorem LiebThirring.measurableSet_voronoiFace {M : ℕ} (R : Fin M → Position) (k l : Fin M) : MeasurableSet (voronoiFace R k l)

theorem LiebThirring.bisectorPlane_eq_affinePlane {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : bisectorPlane R k l = affinePlane (bisectorNormal R k l) (midpoint ℝ (R k) (R l))

theorem LiebThirring.planeHeight_bisector {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : planeHeight (bisectorNormal R k l) (midpoint ℝ (R k) (R l)) (R k) = nuclearHalfDistance R k l

theorem LiebThirring.nuclearHalfDistance_le_norm_on_bisector {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) {y : Position} (hy : y ∈ bisectorPlane R k l) : nuclearHalfDistance R k l ≤ ‖y - R k‖

noncomputable def LiebThirring.bisectorSurfaceFrame {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : PlaneFrame (affinePlane (bisectorNormal R k l) (midpoint ℝ (R k) (R l)))

A frame chosen only to construct surface measure; its measure is independent of this choice, as established by bisectorSurfaceMeasure_eq.

Equations

• LiebThirring.bisectorSurfaceFrame R hR k l hkl = Classical.choice ⋯

noncomputable def LiebThirring.bisectorSurfaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : MeasureTheory.Measure Position

The usual Euclidean surface measure on a bisector plane.

Equations

• LiebThirring.bisectorSurfaceMeasure R hR k l hkl = LiebThirring.planeMeasure (LiebThirring.bisectorSurfaceFrame R hR k l hkl)

theorem LiebThirring.planeMeasure_eq_of_plane_eq {H K : AffineSubspace ℝ Position} [Nonempty ↥H] [Nonempty ↥K] (h : H = K) (F : PlaneFrame H) (G : PlaneFrame K) : planeMeasure F = planeMeasure G