NRR.TestMap.EquivarianceCore — power-partition relabelling

This module proves that the canonical normalized weights, power-partition pieces, perimeter vector, and perimeter deviation commute with relabelling of sites.

theorem NRR.PowerDiagram.cell_relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) (t : Fin n → E2) (u : Fin n → ℝ) (i : Fin n) : cell (fun (j : Fin n) => t ((Equiv.symm σ) j)) (fun (j : Fin n) => u ((Equiv.symm σ) j)) i = cell t u ((Equiv.symm σ) i)

Power cell relabeling. Precomposing both the sites and the weights by σ.symm reindexes the power cell: the i-th cell of the relabeled data is the σ.symm i-th cell of the original data. This is because powerDist (t∘σ.symm) (u∘σ.symm) i x = powerDist t u (σ.symm i) x and the universally-quantified j in the cell condition ranges bijectively via σ.symm.

theorem NRR.PowerDiagram.bodyCellSet_relabel {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (σ : Equiv.Perm (Fin n)) (t : Fin n → Geometry.Plane) (u : Fin n → ℝ) (i : Fin n) : bodyCellSet K (fun (j : Fin n) => t ((Equiv.symm σ) j)) (fun (j : Fin n) => u ((Equiv.symm σ) j)) i = bodyCellSet K t u ((Equiv.symm σ) i)

Restricted power cell relabeling. The restricted cell (intersection with the body K) relabels by σ.symm, inheriting the relabeling of the underlying power cell.

theorem NRR.EMP.normalizedWeight_relabel {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (hn : 0 < n) (σ : Equiv.Perm (Fin n)) (s : Config n) : normalizedWeight K (Config.relabel σ s).pts hn ⋯ = fun (i : Fin n) => normalizedWeight K s.pts hn ⋯ ((Equiv.symm σ) i)

Normalized equal-area weight relabeling. The canonical normalized equal-area weight of the relabeled configuration equals the original normalized weight reindexed by σ.symm. Proved by EMP.normalizedWeight_unique: the reindexed weight w ∘ σ.symm is again equal-area (via PowerDiagram.bodyCellSet_relabel, hence each restricted cell area is unchanged) and normalized (the sum is invariant under reindexing), so by uniqueness it is the normalized weight of the relabeled configuration.

theorem NRR.EMP.powerPartitionPerimeterVec_relabel {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (hn : 0 < n) (hK : 0 < K.area) (σ : Equiv.Perm (Fin n)) (s : Config n) : powerPartitionPerimeterVec K (Config.relabel σ s) hn hK = fun (i : Fin n) => powerPartitionPerimeterVec K s hn hK ((Equiv.symm σ) i)

Power-partition perimeter-vector relabelling. The canonical equal-area power-partition perimeter vector relabels by σ.symm: the perimeter vector of the relabeled configuration is the original perimeter vector precomposed with σ.symm.

This theorem is proved and is the main input to test-map equivariance.

Proof outline: expand the perimeter vector to the perimeter of the i-th power-partition piece, whose carrier is a restricted power cell of the canonical normalized weight. By EMP.normalizedWeight_relabel the weight of the relabeled configuration reindexes by σ.symm, and by PowerDiagram.bodyCellSet_relabel the restricted cell of the relabeled configuration coincides with the σ.symm i-th restricted cell of the original configuration. Since the planar perimeter depends only on the underlying set (NRR.Geometry.planarPerimeter_congr), the perimeters agree.