NRR.PowerDiagram.Defs — core definitions

Base definitions for the power-diagram API: the power (Laguerre) distance powerDist and the power cell cell of a site.

These definitions are isolated so that the implementation modules under NRR/PowerDiagram/ can depend on the core definitions, while the top-level NRR.PowerDiagram re-exports the full, proved API (see NRR/PowerDiagram.lean). This breaks what would otherwise be an import cycle.

Given n sites s : Fin n → E2 and weights w : Fin n → ℝ, the power cell of site i is {x : ∀ j, ‖x - sᵢ‖² - wᵢ ≤ ‖x - sⱼ‖² - wⱼ}.

noncomputable def NRR.PowerDiagram.powerDist {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) (i : Fin n) (x : E2) : ℝ

Power (Laguerre) distance of x to site i with weight w i.

Equations

• NRR.PowerDiagram.powerDist s w i x = ‖x - s i‖ ^ 2 - w i

noncomputable def NRR.PowerDiagram.cell {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) (i : Fin n) : Set E2

Power cell of site i: the points closer (in power distance) to i than to any j.

Equations

• NRR.PowerDiagram.cell s w i = {x : NRR.E2 | ∀ (j : Fin n), NRR.PowerDiagram.powerDist s w i x ≤ NRR.PowerDiagram.powerDist s w j x}