NRR.EMP.PowerPartitionPerimeter — perimeter vector of the canonical power partition

This module specializes the generic convex-partition perimeter API (NRR.ConvexPartition.perimeterVec, averagePerimeter, perimeterDeviation) to the canonical equal-area power partition EMP.powerPartition.

The power-partition parameter profile is the one fixed in the project:

(K : Geometry.ConvexBody Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area)

Public API

• EMP.powerPartitionPerimeterVec — the perimeter vector of the canonical power partition.
• EMP.powerPartitionAveragePerimeter — its average perimeter.
• EMP.powerPartitionPerimeterDeviation — its perimeter-deviation vector.
• EMP.powerPartitionPerimeterVec_apply — the defining simp lemma for the perimeter vector.
• EMP.sum_powerPartitionPerimeterDeviation_eq_zero — the deviation vector sums to zero.

No continuity, equivariance, or test-map material is introduced here.

noncomputable def NRR.EMP.powerPartitionPerimeterVec {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : Fin n → ℝ

The perimeter vector of the canonical equal-area power partition.

Equations

• NRR.EMP.powerPartitionPerimeterVec K s hn hK = (NRR.EMP.powerPartition K s hn hK).perimeterVec

noncomputable def NRR.EMP.powerPartitionAveragePerimeter {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : ℝ

The average perimeter of the canonical equal-area power partition.

Equations

• NRR.EMP.powerPartitionAveragePerimeter K s hn hK = (NRR.EMP.powerPartition K s hn hK).averagePerimeter

noncomputable def NRR.EMP.powerPartitionPerimeterDeviation {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : Fin n → ℝ

The perimeter-deviation vector of the canonical equal-area power partition.

Equations

• NRR.EMP.powerPartitionPerimeterDeviation K s hn hK = (NRR.EMP.powerPartition K s hn hK).perimeterDeviation

@[simp]

theorem NRR.EMP.powerPartitionPerimeterVec_apply {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) (i : Fin n) : powerPartitionPerimeterVec K s hn hK i = Geometry.ConvexBody.perimeter ((powerPartition K s hn hK).piece i)

The i-th entry of the power-partition perimeter vector is the perimeter of its i-th piece.

theorem NRR.EMP.sum_powerPartitionPerimeterDeviation_eq_zero {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : ∑ i : Fin n, powerPartitionPerimeterDeviation K s hn hK i = 0

The perimeter-deviation vector of the canonical equal-area power partition sums to zero.