NRR.EMP.VariableBody.Partition — the variable-body equal-area power partition

For a compact metric parameter space X carrying a continuous site family sites : SiteFamily X n, a positive lower area A, and 0 < n, this module exposes the canonical equal-area power partition of each variable solid body solidBody hA z.1 as a thin wrapper around EMP.powerPartition. Its pieces are propositionally identified with the continuously varying child bodies child sites hA hn z i packaged in Children.lean.

Continuity of the family is carried entirely by child (and its continuity results); the dependent partition field is not asserted to be continuous, and no topology is placed on ConvexPartition (solidBody hA z.1) n.

• partition — the canonical equal-area power partition of the variable solid body.
• partition_isEqualArea, partition_covers, partition_nullOverlap — the three partition facts, reused verbatim from the fixed-body power-partition API.
• partition_piece_carrier_eq_child — each piece's carrier is exactly the corresponding child body.
• partition_piece_area_eq — each piece has area z.1.body.area / n.
• Witness / witness — the partition packaged together with its children and all partition facts, as consumed by the prime-refinement layer.

noncomputable def NRR.EMP.VariableBody.partition {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : ConvexPartition (solidBody hA z.1) n

The canonical equal-area power partition of the variable solid body solidBody hA z.1, computed with the site configuration sites z.2. A thin wrapper around EMP.powerPartition.

Equations

• NRR.EMP.VariableBody.partition sites hA hn z = NRR.EMP.powerPartition (NRR.EMP.VariableBody.solidBody hA z.1) (sites z.2) hn ⋯

theorem NRR.EMP.VariableBody.partition_isEqualArea {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : (partition sites hA hn z).IsEqualArea

Equal area. Every piece of the variable partition has the same area.

theorem NRR.EMP.VariableBody.partition_covers {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : (solidBody hA z.1).carrier ⊆ ⋃ (i : Fin n), ((partition sites hA hn z).piece i).carrier

Cover. The pieces of the variable partition cover the variable solid body.

theorem NRR.EMP.VariableBody.partition_nullOverlap {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) (i j : Fin n) (hij : i ≠ j) : MeasureTheory.volume (((partition sites hA hn z).piece i).carrier ∩ ((partition sites hA hn z).piece j).carrier) = 0

Null overlap. Distinct pieces of the variable partition overlap only on a Lebesgue-null set.

theorem NRR.EMP.VariableBody.partition_piece_carrier_eq_child {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) (i : Fin n) : ((partition sites hA hn z).piece i).carrier = ↑(child sites hA hn z i).body.body

Piece compatibility. The carrier of the i-th piece of the variable partition is exactly the carrier of the i-th canonical child body, both being the restricted power cell of the canonical normalized equal-area weight.

theorem NRR.EMP.VariableBody.partition_piece_area_eq {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) (i : Fin n) : Geometry.ConvexBody.area ((partition sites hA hn z).piece i) = z.1.body.area / ↑n

Piece area. Each piece of the variable partition has area z.1.body.area / n.

structure NRR.EMP.VariableBody.Witness {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : Type

The partition witness at a parameter z: the canonical variable-body power partition together with its continuously varying children and all the partition facts a refinement step needs. Continuity of the family is carried by the child field (see continuous_child), not by the dependent partition field.

• partition : ConvexPartition (solidBody hA z.1) n

  The canonical equal-area power partition of the variable solid body.

• child : Fin n → BodySpace K (A / ↑n)

  The continuously varying child bodies, one per piece.

• piece_eq (i : Fin n) : (self.partition.piece i).carrier = ↑(self.child i).body.body

  Each piece agrees, as a set, with the corresponding child body.

• equalArea : self.partition.IsEqualArea

  All pieces have equal area.

• covers : (solidBody hA z.1).carrier ⊆ ⋃ (i : Fin n), (self.partition.piece i).carrier

  The pieces cover the variable solid body.

• nullOverlap (i j : Fin n) : i ≠ j → MeasureTheory.volume ((self.partition.piece i).carrier ∩ (self.partition.piece j).carrier) = 0

  Distinct pieces overlap only on a null set.

noncomputable def NRR.EMP.VariableBody.witness {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : Witness sites hA hn z

The canonical partition witness at z, built from the existing variable-body partition and its canonical children. No partition proof is duplicated: every field reuses the corresponding partition_* fact.

Equations

• One or more equations did not get rendered due to their size.