NRR.PowerDiagram.CellAreaVector — the restricted power‑cell area vector

Packaging the (fixed‑site) restricted power‑cell areas of a convex body K into a single vector‑valued map

PowerDiagram.areaVec K s w = fun i => bodyCellArea K s w i : Fin n → ℝ.

The two headline facts, both with fixed sites:

• continuous_areaVec_weights — the vector w ↦ areaVec K s w is continuous in the weights.
• sum_areaVec_eq_area — under distinct sites its total mass is the body area K.area.

Necessary nondegeneracy hypotheses

Both statements carry hs : Function.Injective s. This is not optional:

• Continuity specializes the fixed‑site component result continuous_bodyCellArea_weights, which is genuinely false when two sites coincide (the offending halfspace collapses to {x | w i ≥ w j}, producing a jump discontinuity of the area as w i crosses w j). Injectivity supplies the required s j ≠ s i for every j ≠ i.
• The total‑mass identity uses the almost‑disjoint covering of K by the restricted cells (iUnion_bodyCellSet, bodyCellSet_inter_null); the null‑overlap step needs distinct sites.

The total‑mass identity additionally needs at least one site ([NeZero n]): with no sites the cells cover nothing while a convex body has positive area, so the n = 0 claim is false.

Sites are held fixed throughout; nothing here assumes cells are nonempty, and no equal‑area statement is proved.

noncomputable def NRR.PowerDiagram.areaVec {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) : Fin n → ℝ

Restricted power‑cell area vector. With sites s and weights w, the i‑th component is the restricted‑cell area bodyCellArea K s w i.

Equations

• NRR.PowerDiagram.areaVec K s w i = NRR.PowerDiagram.bodyCellArea K s w i

@[simp]

theorem NRR.PowerDiagram.areaVec_apply {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : areaVec K s w i = bodyCellArea K s w i

The i‑th component of areaVec is the restricted‑cell area.

theorem NRR.PowerDiagram.continuous_areaVec_weights {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hs : Function.Injective s) : Continuous fun (w : Fin n → ℝ) => areaVec K s w

Fixed‑site weight‑continuity of the area vector. With sites s fixed and pairwise distinct (hs), the vector‑valued area map w ↦ areaVec K s w is continuous in the weights. The injectivity hypothesis is necessary (see the module docstring).

theorem NRR.PowerDiagram.sum_areaVec_eq_area {n : ℕ} [NeZero n] (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hs : Function.Injective s) : ∑ i : Fin n, areaVec K s w i = K.area

Total mass of the area vector. For distinct sites (hs) and at least one site ([NeZero n]), the areas of the restricted power cells sum to the body area K.area.