NRR.EMP.VariableBody.AreaVector — the variable-body area vector

The scalar cell-area continuity of CellAreaContinuity is lifted to the finite area vector areaVec hA C s w : Fin n → ℝ, whose i-th component is the restricted power-cell area cellArea hA C s w i. The target area targetArea C n = C.body.area / n is the common value that an equal-area weight assigns to every cell.

• areaVec — the vector of restricted cell areas.
• targetArea — the average cell area C.body.area / n.
• continuous_areaVec — joint continuity of the area vector in body, sites, and weights.
• continuous_targetArea — continuity of the average area in the parent subbody.

noncomputable def NRR.EMP.VariableBody.areaVec {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) : Fin n → ℝ

The area vector of the variable body C for sites s and weights w: the vector whose i-th component is the area of the restricted power cell of site i.

Equations

• NRR.EMP.VariableBody.areaVec hA C s w i = NRR.EMP.VariableBody.cellArea hA C s w i

noncomputable def NRR.EMP.VariableBody.targetArea {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) (n : ℕ) : ℝ

The target area for an equal-area partition of the variable body C into n cells: the average cell area C.body.area / n.

Equations

• NRR.EMP.VariableBody.targetArea C n = C.body.area / ↑n

@[simp]

theorem NRR.EMP.VariableBody.areaVec_apply {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) : areaVec hA C s w i = cellArea hA C s w i

theorem NRR.EMP.VariableBody.continuous_areaVec {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) : Continuous fun (z : BodySpace K A × Config n × (Fin n → ℝ)) => areaVec hA z.1 z.2.1 z.2.2

Joint continuity of the area vector. The finite vector of restricted cell areas depends continuously on the parent subbody, the configuration, and the weight vector.

theorem NRR.EMP.VariableBody.continuous_targetArea {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} : Continuous fun (C : BodySpace K A) => targetArea C n

Continuity of the target area. The average cell area depends continuously on the parent subbody through the continuity of the area functional.