Finite-indexed convex partitions

The prime-refinement iteration naturally produces nested product index types. This file provides an index-polymorphic version of ConvexPartition and a canonical conversion back to the public Fin n-indexed structure.

structure NRR.IndexedConvexPartition (K : Body) (ι : Type u_1) : Type u_1

A convex partition indexed by an arbitrary type. Finiteness is only required when converting back to the public ConvexPartition structure.

• piece : ι → Body

  The convex body assigned to each index of the partition.

• subset (i : ι) : (self.piece i).carrier ⊆ K.carrier
• covers : K.carrier ⊆ ⋃ (i : ι), (self.piece i).carrier
• nullOverlap (i j : ι) : i ≠ j → MeasureTheory.volume ((self.piece i).carrier ∩ (self.piece j).carrier) = 0

def NRR.IndexedConvexPartition.IsEqualArea {K : Body} {ι : Type u_1} (P : IndexedConvexPartition K ι) : Prop

All indexed pieces have equal area.

Equations

• P.IsEqualArea = ∀ (i j : ι), NRR.Geometry.ConvexBody.area (P.piece i) = NRR.Geometry.ConvexBody.area (P.piece j)

def NRR.IndexedConvexPartition.HasEqualPerimeter {K : Body} {ι : Type u_1} (P : IndexedConvexPartition K ι) : Prop

All indexed pieces have equal perimeter.

Equations

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

def NRR.IndexedConvexPartition.ofConvexPartition {K : Body} {n : ℕ} (P : ConvexPartition K n) : IndexedConvexPartition K (Fin n)

Regard an ordinary Fin n-indexed partition as an indexed partition.

Equations

• NRR.IndexedConvexPartition.ofConvexPartition P = { piece := P.piece, subset := ⋯, covers := ⋯, nullOverlap := ⋯ }

noncomputable def NRR.IndexedConvexPartition.singleton (K : Body) : IndexedConvexPartition K Unit

The singleton indexed partition.

Equations

• NRR.IndexedConvexPartition.singleton K = { piece := fun (x : Unit) => K, subset := ⋯, covers := ⋯, nullOverlap := ⋯ }

def NRR.IndexedConvexPartition.castBody {K L : Body} {ι : Type u_1} (h : K = L) (P : IndexedConvexPartition K ι) : IndexedConvexPartition L ι

Change the ambient body along an equality.

Equations

• NRR.IndexedConvexPartition.castBody h P = h ▸ P

theorem NRR.IndexedConvexPartition.castBody_isEqualArea {K L : Body} {ι : Type u_1} (h : K = L) (P : IndexedConvexPartition K ι) : (castBody h P).IsEqualArea ↔ P.IsEqualArea

Equal area is invariant under changing only the ambient body by equality.

theorem NRR.IndexedConvexPartition.castBody_hasEqualPerimeter {K L : Body} {ι : Type u_1} (h : K = L) (P : IndexedConvexPartition K ι) : (castBody h P).HasEqualPerimeter ↔ P.HasEqualPerimeter

Equal perimeter is invariant under changing only the ambient body by equality.

def NRR.IndexedConvexPartition.reindex {K : Body} {ι : Type u_1} {κ : Type u_2} (P : IndexedConvexPartition K ι) (e : κ ≃ ι) : IndexedConvexPartition K κ

Reindex a partition along an equivalence.

Equations

• P.reindex e = { piece := fun (i : κ) => P.piece (e i), subset := ⋯, covers := ⋯, nullOverlap := ⋯ }

noncomputable def NRR.IndexedConvexPartition.toConvexPartition {K : Body} {ι : Type u_1} [Fintype ι] (P : IndexedConvexPartition K ι) : ConvexPartition K (Fintype.card ι)

Convert a finite indexed partition to the public Fin (card ι)-indexed partition.

Equations

• P.toConvexPartition = { piece := fun (i : Fin (Fintype.card ι)) => P.piece ((Fintype.equivFin ι).symm i), subset := ⋯, covers := ⋯, nullOverlap := ⋯ }

theorem NRR.IndexedConvexPartition.reindex_isEqualArea {K : Body} {ι : Type u_1} {κ : Type u_2} (P : IndexedConvexPartition K ι) (e : κ ≃ ι) (hP : P.IsEqualArea) : (P.reindex e).IsEqualArea

Equal area is preserved by reindexing.

theorem NRR.IndexedConvexPartition.reindex_hasEqualPerimeter {K : Body} {ι : Type u_1} {κ : Type u_2} (P : IndexedConvexPartition K ι) (e : κ ≃ ι) (hP : P.HasEqualPerimeter) : (P.reindex e).HasEqualPerimeter

Equal perimeter is preserved by reindexing.

theorem NRR.IndexedConvexPartition.toConvexPartition_isEqualArea {K : Body} {ι : Type u_1} [Fintype ι] (P : IndexedConvexPartition K ι) (hP : P.IsEqualArea) : P.toConvexPartition.IsEqualArea

Conversion to ConvexPartition preserves equal area.

theorem NRR.IndexedConvexPartition.toConvexPartition_hasEqualPerimeter {K : Body} {ι : Type u_1} [Fintype ι] (P : IndexedConvexPartition K ι) (hP : P.HasEqualPerimeter) : P.toConvexPartition.HasEqualPerimeter

Conversion to ConvexPartition preserves equal perimeter.