NRR.EMP.VariableBody.CanonicalCellGraph — one-sided closedness of the cell graph

We record the one-sided closed-graph property of the canonical power cell: the relation

{z | (z.2.body : Set Plane) ⊆ (canonicalCell sites hA hn z.1 i).body}

over (BodySpace K A × X) × ConvexSubbody K is closed. Concretely, if a sequence of subbodies D_m contained in the canonical cell at parameters z_m converges (in the Hausdorff metric) to D, while z_m → z, then D is contained in the canonical cell at z.

The proof is the sequential closed-set criterion. A point y ∈ D is approximated by points y_m ∈ D_m (ConvexSubbody.exists_tendsto_points); each y_m lies in the moving cell, so it lies in the moving parent body and satisfies every off-diagonal power-halfspace inequality. Parent membership passes to the limit via ConvexSubbody.mem_limit_of_tendsto; each halfspace inequality passes to the limit by continuity of the separating normal (in the sites) and offset (in the sites and the selected weight, through continuous_normalizedWeight_compactFamily) together with closedness of ≤. Hence y lies in the limiting cell.

theorem NRR.EMP.VariableBody.mem_canonicalCell_iff {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) (y : Geometry.Plane) : y ∈ ↑(canonicalCell sites hA hn z i).body ↔ y ∈ ↑z.1.body.body ∧ ∀ (j : { j : Fin n // j ≠ i }), inner ℝ (sepNormal (sites z.2) i ↑j) y ≤ sepOffset (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) i ↑j

Halfspace membership characterization of the canonical cell. A point lies in the canonical power cell iff it lies in the parent body and satisfies every off-diagonal power-halfspace inequality.

def NRR.EMP.VariableBody.CanonicalCellLowerGraph {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (i : Fin n) : Set ((BodySpace K A × X) × ConvexSubbody K)

The one-sided (lower) canonical-cell graph: parameter–subbody pairs (z, D) where the subbody D is contained in the canonical power cell of site i at z.

Equations

• NRR.EMP.VariableBody.CanonicalCellLowerGraph sites hA hn i = {z : (NRR.BodySpace K A × X) × NRR.ConvexSubbody K | ↑z.2.body ⊆ ↑(NRR.EMP.VariableBody.canonicalCell sites hA hn z.1 i).body}

theorem NRR.EMP.VariableBody.isClosed_canonicalCellLowerGraph {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (i : Fin n) : IsClosed (CanonicalCellLowerGraph sites hA hn i)