Voronoi cells and strict faces

The perpendicular bisector affine subspace of two nuclei.

Points having nucleus k as their unique closest nucleus.

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

The perpendicular bisector affine subspace of two nuclei.

Equations

• LiebThirring.bisectorPlane R k l = AffineSubspace.perpBisector (R k) (R l)

def LiebThirring.voronoiCell {M : ℕ} (R : Fin M → Position) (k : Fin M) : Set Position

Points having nucleus k as their unique closest nucleus.

Equations

• LiebThirring.voronoiCell R k = {x : LiebThirring.Position | ∀ (l : Fin M), l ≠ k → dist x (R k) < dist x (R l)}

def LiebThirring.closedVoronoiCell {M : ℕ} (R : Fin M → Position) (k : Fin M) : Set Position

Points having nucleus k among their closest nuclei.

Equations

• LiebThirring.closedVoronoiCell R k = {x : LiebThirring.Position | ∀ (l : Fin M), dist x (R k) ≤ dist x (R l)}

def LiebThirring.voronoiFace {M : ℕ} (R : Fin M → Position) (k l : Fin M) : Set Position

The genuine face: exactly k and l are closest, with no third tie.

Equations

• LiebThirring.voronoiFace R k l = {x : LiebThirring.Position | k ≠ l ∧ x ∈ LiebThirring.bisectorPlane R k l ∧ ∀ (p : Fin M), p ≠ k → p ≠ l → dist x (R k) < dist x (R p)}

def LiebThirring.voronoiTripleStratum {M : ℕ} (R : Fin M → Position) : Set Position

The finite union of intersections of bisectors with a common nucleus. It contains every point with at least three nearest nuclei.

Equations

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

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

The directed unit bisector normal for distinct nuclei.

Equations

• LiebThirring.bisectorNormal R k l = ‖R l - R k‖⁻¹ • (R l - R k)

@[simp]

theorem LiebThirring.mem_bisectorPlane {M : ℕ} (R : Fin M → Position) (k l : Fin M) (x : Position) : x ∈ bisectorPlane R k l ↔ dist x (R k) = dist x (R l)

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

theorem LiebThirring.dist_lt_dist_iff_inner_lt (x a b : Position) : dist x a < dist x b ↔ 2 * inner ℝ (b - a) (x - a) < ‖b - a‖ ^ 2

Squared-distance comparison, in affine-linear form.

theorem LiebThirring.dist_le_dist_iff_inner_le (x a b : Position) : dist x a ≤ dist x b ↔ 2 * inner ℝ (b - a) (x - a) ≤ ‖b - a‖ ^ 2

theorem LiebThirring.mem_voronoiCell_iff_inner {M : ℕ} (R : Fin M → Position) (k : Fin M) (x : Position) : x ∈ voronoiCell R k ↔ ∀ (l : Fin M), l ≠ k → 2 * inner ℝ (R l - R k) (x - R k) < ‖R l - R k‖ ^ 2

theorem LiebThirring.voronoiCell_subset_closed {M : ℕ} (R : Fin M → Position) (k : Fin M) : voronoiCell R k ⊆ closedVoronoiCell R k

theorem LiebThirring.isOpen_voronoiCell {M : ℕ} (R : Fin M → Position) (k : Fin M) : IsOpen (voronoiCell R k)

theorem LiebThirring.disjoint_voronoiCell {M : ℕ} (R : Fin M → Position) {k l : Fin M} (hkl : k ≠ l) : Disjoint (voronoiCell R k) (voronoiCell R l)

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

theorem LiebThirring.voronoiFace_subset_closed {M : ℕ} (R : Fin M → Position) (k l : Fin M) : voronoiFace R k l ⊆ closedVoronoiCell R k

theorem LiebThirring.nearestNucleusDistance_eq_of_mem_closedVoronoiCell {M : ℕ} (R : Fin M → Position) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : nearestNucleusDistance R x = ENNReal.ofReal ‖x - R k‖

@[simp]

theorem LiebThirring.nearestOtherNucleusDistance_one (R : Fin 1 → Position) (k : Fin 1) : nearestOtherNucleusDistance R k = ⊤