NRR.EMP.VariableBody.Children — canonical children in the lower-area BodySpace

Each canonical power cell canonicalCell sites hA hn z i has area exactly z.1.body.area / n, and z.1.body.area ≥ A, so the cell area is at least A / n. This lets us package every canonical cell as a genuine element of the lower-area hyperspace BodySpace K (A / (n : ℝ)).

• child — the canonical cell packaged in BodySpace K (A / (n : ℝ)).
• child_body, child_area_eq, child_subset_parent, child_lower_area, child_lower_bound_pos — the basic bookkeeping of the child body.
• continuous_child, continuous_children — Hausdorff continuity of the child family, obtained by packaging continuous_canonicalCell through the subtype constructor of BodySpace.
• continuous_child_area — continuity of the child area, from the continuous area map.
• continuous_child_perimeter, continuous_child_perimeters — continuity of the child perimeter as a direct composition through the solid bridge BodySpace.toGeometryConvexBody.

theorem NRR.EMP.VariableBody.child_lower_bound_pos {n : ℕ} {A : ℝ} (hA : 0 < A) (hn : 0 < n) : 0 < A / ↑n

Positivity of the child lower area. When 0 < A and 0 < n, the lower area A / n of the child hyperspace is strictly positive.

noncomputable def NRR.EMP.VariableBody.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) : BodySpace K (A / ↑n)

The canonical child of site i: the canonical power cell of the parameter z, packaged as an element of the lower-area hyperspace BodySpace K (A / (n : ℝ)). The lower-area condition follows from A ≤ z.1.body.area, 0 < n, and canonicalCell.area = z.1.body.area / n.

Equations

• NRR.EMP.VariableBody.child sites hA hn z i = ⟨NRR.EMP.VariableBody.canonicalCell sites hA hn z i, ⋯⟩

@[simp]

theorem NRR.EMP.VariableBody.child_body {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) : (child sites hA hn z i).body = canonicalCell sites hA hn z i

theorem NRR.EMP.VariableBody.child_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) : (child sites hA hn z i).body.area = z.1.body.area / ↑n

theorem NRR.EMP.VariableBody.child_subset_parent {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) : ↑(child sites hA hn z i).body.body ⊆ K.carrier

theorem NRR.EMP.VariableBody.child_lower_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) : A / ↑n ≤ (child sites hA hn z i).body.area

theorem NRR.EMP.VariableBody.continuous_child {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) : Continuous fun (z : BodySpace K A × X) => child sites hA hn z i

Continuity of the child. Each canonical child depends continuously on the parameter, valued in the compact Hausdorff hyperspace BodySpace K (A / (n : ℝ)).

theorem NRR.EMP.VariableBody.continuous_children {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) : Continuous fun (z : BodySpace K A × X) (i : Fin n) => child sites hA hn z i

Continuity of the child family. The whole finite family of canonical children depends continuously on the parameter.

theorem NRR.EMP.VariableBody.continuous_child_area {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) : Continuous fun (z : BodySpace K A × X) => (child sites hA hn z i).body.area

Continuity of the child area. The area of each child varies continuously in the parameter, by composing continuous_child with the continuous area map.

theorem NRR.EMP.VariableBody.continuous_child_perimeter {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) : Continuous fun (z : BodySpace K A × X) => ((child sites hA hn z i).toGeometryConvexBody ⋯).perimeter

Continuity of the child perimeter. The planar (Cauchy) perimeter of each child's solid bridge varies continuously, as a direct composition: continuous_child, BodySpace.continuous_perimeter at lower bound A / (n : ℝ).

theorem NRR.EMP.VariableBody.continuous_child_perimeters {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) : Continuous fun (z : BodySpace K A × X) (i : Fin n) => ((child sites hA hn z i).toGeometryConvexBody ⋯).perimeter

Continuity of the child perimeter family. The whole finite family of child perimeters depends continuously on the parameter.