Convex-body interface for variable-body power partitions

This module re-exports the convex-body hyperspace API used by the variable-body power-partition construction and defines its parameter-space conventions.

Re-exported convex-body interface

The interface includes compactness of ConvexSubbody and BodySpace, continuity of area and of the body projection, positivity at a positive area threshold, and membership stability under Hausdorff convergence. The metric is Mathlib's Hausdorff metric inherited through TopologicalSpace.NonemptyCompacts Plane; no competing metric or topology is introduced.

Body projections

• NRR.BodySpace.body : BodySpace K A → ConvexSubbody K lands in the fixed-parent hyperspace, whose elements may be lower-dimensional.
• NRR.BodySpace.toGeometryConvexBody (hA : 0 < A) lands in the solid planar convex-body type and is continuous.

Parameterization

Continuity results are stated over a compact metric parameter space X carrying a continuous site family sites : C(X, Config n). The configuration space Config n itself is not assumed compact.

@[reducible, inline]

abbrev NRR.EMP.VariableBody.SiteFamily (X : Type u_1) [TopologicalSpace X] (n : ℕ) : Type u_1

A continuous site family over a parameter space X: a continuous map assigning to each parameter a configuration of n distinct labelled planar sites. Continuity results use a compact metric X; Config n itself is not assumed compact.

Equations

• NRR.EMP.VariableBody.SiteFamily X n = C(X, NRR.Config n)

@[reducible, inline]

abbrev NRR.EMP.VariableBody.Param (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) (X : Type u_1) : Type u_1

The variable-body parameter space: the compact convex-body factor BodySpace K A paired with an auxiliary parameter space X, typically the site-family parameter.

Equations

• NRR.EMP.VariableBody.Param K A X = (NRR.BodySpace K A × X)