Voronoi cells as finite halfspace slices

The affine constraints and genuine-facet values needed to instantiate the scalar fundamental theorem on almost every coordinate line.

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

The affine offset of a Voronoi halfspace along a selected coordinate line.

Equations

• LiebThirring.voronoiSliceOffset R k l a q = ‖R l - R k‖ / 2 - inner ℝ (LiebThirring.bisectorNormal R k l) (LiebThirring.coordinateLine a q 0 - R k)

theorem LiebThirring.inner_bisectorNormal_coordinateLine {M : ℕ} (R : Fin M → Position) (k l : Fin M) (a : Fin 3) (q : Planar) (t : ℝ) : inner ℝ (bisectorNormal R k l) (coordinateLine a q t - R k) = t * (bisectorNormal R k l).ofLp a + inner ℝ (bisectorNormal R k l) (coordinateLine a q 0 - R k)

theorem LiebThirring.dist_lt_dist_iff_bisectorNormal {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (x : Position) : dist x (R k) < dist x (R l) ↔ inner ℝ (bisectorNormal R k l) (x - R k) < ‖R l - R k‖ / 2

theorem LiebThirring.dist_lt_dist_coordinateLine_iff {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (a : Fin 3) (q : Planar) (t : ℝ) : dist (coordinateLine a q t) (R k) < dist (coordinateLine a q t) (R l) ↔ t * (bisectorNormal R k l).ofLp a < voronoiSliceOffset R k l a q

theorem LiebThirring.mem_voronoiCell_coordinateLine_iff {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (a : Fin 3) (q : Planar) (t : ℝ) : coordinateLine a q t ∈ voronoiCell R k ↔ ∀ (l : { l : Fin M // l ≠ k }), t * (bisectorNormal R k ↑l).ofLp a < voronoiSliceOffset R k (↑l) a q

theorem LiebThirring.coordinateLine_slice_root_mem_bisector {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (a : Fin 3) (q : Planar) (ha : (bisectorNormal R k l).ofLp a ≠ 0) : coordinateLine a q (voronoiSliceOffset R k l a q / (bisectorNormal R k l).ofLp a) ∈ bisectorPlane R k l

theorem LiebThirring.voronoi_slice_constraints_regular {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (a : Fin 3) (q : Planar) (hq : q ∉ slicingExceptionalSet R a) (t : ℝ) (l p : { l : Fin M // l ≠ k }) (hlp : l ≠ p) (hl : t * (bisectorNormal R k ↑l).ofLp a = voronoiSliceOffset R k (↑l) a q) (hp : t * (bisectorNormal R k ↑p).ofLp a = voronoiSliceOffset R k (↑p) a q) : False

theorem LiebThirring.coordinateLine_slice_root_eq_planeGraph {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (a : Fin 3) (q : Planar) (ha : (bisectorNormal R k l).ofLp a ≠ 0) : coordinateLine a q (voronoiSliceOffset R k l a q / (bisectorNormal R k l).ofLp a) = planeGraph (bisectorNormal R k l) (midpoint ℝ (R k) (R l)) a ha q

theorem LiebThirring.halfspaceFaceValue_voronoi {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (l : { l : Fin M // l ≠ k }) (a : Fin 3) (q : Planar) (ha : (bisectorNormal R k ↑l).ofLp a ≠ 0) (g : Position → ℝ) : halfspaceFaceValue (fun (p : { p : Fin M // p ≠ k }) => (bisectorNormal R k ↑p).ofLp a) (fun (p : { p : Fin M // p ≠ k }) => voronoiSliceOffset R k (↑p) a q) (fun (t : ℝ) => g (coordinateLine a q t)) l = (voronoiFace R k ↑l).indicator g (coordinateLine a q (voronoiSliceOffset R k (↑l) a q / (bisectorNormal R k ↑l).ofLp a))