NRR.Partition.PerimeterVector — perimeter vector of a convex partition

For a convex partition P : ConvexPartition K n this module records the elementary perimeter data of P:

• ConvexPartition.perimeterVec — the Fin n → ℝ vector of piece perimeters;
• ConvexPartition.totalPerimeter — the sum of the piece perimeters;
• ConvexPartition.averagePerimeter — the total perimeter divided by (n : ℝ).

The underlying perimeter is the public planar Cauchy perimeter NRR.Geometry.ConvexBody.perimeter from NRR.AreaPerimeter. The pieces of a ConvexPartition have type Body = Geometry.ConvexBody Plane, so this perimeter applies directly to each piece.

No equal-area assumption, test map, or continuity statement is introduced here: this module is purely the definitional perimeter API.

noncomputable def NRR.ConvexPartition.perimeterVec {K : Body} {n : ℕ} (P : ConvexPartition K n) : Fin n → ℝ

The perimeter vector of a convex partition: the i-th entry is the perimeter of the i-th piece.

Equations

• P.perimeterVec i = NRR.Geometry.ConvexBody.perimeter (P.piece i)

noncomputable def NRR.ConvexPartition.totalPerimeter {K : Body} {n : ℕ} (P : ConvexPartition K n) : ℝ

The total perimeter of a convex partition: the sum of the piece perimeters.

Equations

• P.totalPerimeter = ∑ i : Fin n, P.perimeterVec i

noncomputable def NRR.ConvexPartition.averagePerimeter {K : Body} {n : ℕ} (P : ConvexPartition K n) : ℝ

The average perimeter of a convex partition: the total perimeter divided by (n : ℝ). The division is explicitly by the real cast (n : ℝ).

Equations

• P.averagePerimeter = P.totalPerimeter / ↑n

@[simp]

theorem NRR.ConvexPartition.perimeterVec_apply {K : Body} {n : ℕ} (P : ConvexPartition K n) (i : Fin n) : P.perimeterVec i = Geometry.ConvexBody.perimeter (P.piece i)

theorem NRR.ConvexPartition.totalPerimeter_eq_sum {K : Body} {n : ℕ} (P : ConvexPartition K n) : P.totalPerimeter = ∑ i : Fin n, P.perimeterVec i

theorem NRR.ConvexPartition.averagePerimeter_eq {K : Body} {n : ℕ} (P : ConvexPartition K n) : P.averagePerimeter = P.totalPerimeter / ↑n

noncomputable def NRR.ConvexPartition.perimeterDeviation {K : Body} {n : ℕ} (P : ConvexPartition K n) : Fin n → ℝ

The perimeter-deviation vector of a convex partition: the i-th entry is the deviation of the i-th piece perimeter from the average perimeter.

Equations

• P.perimeterDeviation i = P.perimeterVec i - P.averagePerimeter

def NRR.ConvexPartition.HasEqualPerimeter {K : Body} {n : ℕ} (P : ConvexPartition K n) : Prop

All pieces have equal perimeter.

Equations

• P.HasEqualPerimeter = ∀ (i j : Fin n), NRR.Geometry.ConvexBody.perimeter (P.piece i) = NRR.Geometry.ConvexBody.perimeter (P.piece j)

@[simp]

theorem NRR.ConvexPartition.perimeterDeviation_apply {K : Body} {n : ℕ} (P : ConvexPartition K n) (i : Fin n) : P.perimeterDeviation i = P.perimeterVec i - P.averagePerimeter

theorem NRR.ConvexPartition.sum_perimeterDeviation_eq_zero {K : Body} {n : ℕ} (P : ConvexPartition K n) (hn : 0 < n) : ∑ i : Fin n, P.perimeterDeviation i = 0

The perimeter-deviation vector sums to zero.

noncomputable def NRR.ConvexPartition.perimeterDeviationZeroSum {K : Body} {n : ℕ} (P : ConvexPartition K n) (hn : 0 < n) : ZeroSum n

The perimeter-deviation vector, packaged as an element of the zero-sum target type.

Equations

• P.perimeterDeviationZeroSum hn = ⟨P.perimeterDeviation, ⋯⟩

theorem NRR.ConvexPartition.perimeterDeviation_pointwise_zero_iff {K : Body} {n : ℕ} (P : ConvexPartition K n) (hn : 0 < n) : (∀ (i : Fin n), P.perimeterDeviation i = 0) ↔ P.HasEqualPerimeter

The perimeter deviation vanishes pointwise iff all pieces have equal perimeter.

theorem NRR.ConvexPartition.perimeterDeviation_eq_zero_iff {K : Body} {n : ℕ} (P : ConvexPartition K n) (hn : 0 < n) : P.perimeterDeviation = 0 ↔ P.HasEqualPerimeter

The perimeter deviation is the zero function iff all pieces have equal perimeter.