Documentation

LeanPool.NandakumarRamanaRao.NRR.EMP.VariableBody.CanonicalCell

NRR.EMP.VariableBody.CanonicalCell — the canonical variable-body power cell #

For a compact metric parameter space X carrying a continuous site family sites : SiteFamily X n, a positive lower area A, and 0 < n, we bundle the restricted power cell of site i, computed with the canonical normalized equal-area weight, as a genuine convex subbody of the fixed parent K.

The carrier of canonicalCell sites hA hn z i is exactly the set-level power cell

cellSet hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) i,

which is convex and compact by the general cell API and nonempty because the equal-area property gives it positive area (indeed nonempty interior). The cell area equals the target average area z.1.body.area / n.

source
theorem NRR.EMP.VariableBody.canonicalCell_interior_nonempty {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) :
(interior (cellSet hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) i)).Nonempty

The canonical power cell has nonempty interior: the equal-area property of the selected weight forces positive cell area, hence nonempty interior by the project's positive-area theorem.

source
noncomputable def NRR.EMP.VariableBody.canonicalCell {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) :
ConvexSubbody K

The canonical variable-body power cell of site i: the restricted power cell computed with the canonical normalized equal-area weight, bundled as a convex subbody of the fixed parent K.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NRR.EMP.VariableBody.canonicalCell_carrier {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) :
    ↑(canonicalCell sites hA hn z i).body = cellSet hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) i
    source
    theorem NRR.EMP.VariableBody.canonicalCell_area {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) :
    (canonicalCell sites hA hn z i).area = cellArea hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) i
    source
    theorem NRR.EMP.VariableBody.canonicalCell_area_eq_target {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) :
    (canonicalCell sites hA hn z i).area = z.1.body.area / ↑n