NRR.EMP.VariableBody.CellAreaContinuity — joint continuity of cell area

The restricted power-cell area cellArea hA C s w i depends continuously on the triple (C, s, w) of parent subbody, configuration, and weight vector. The argument is a dominated convergence: the area is the Lebesgue integral of the 0/1 cell indicator, these indicators converge almost everywhere along any convergent filter (tendsto_cell_indicator_ae), and every cell is contained in the fixed parent body K, so the constant parent indicator is an integrable dominating function.

• continuous_cellArea — joint continuity in body, sites, and weights.
• continuous_cellArea_compactFamily — the composition with a continuous site family sites : C(X, Config n), needing only continuity of X, not compactness.

instance NRR.EMP.VariableBody.instFirstCountableTopologyConfig (n : ℕ) : FirstCountableTopology (Config n)

The configuration topology is induced by the point map from the metric space Fin n → E2, hence first countable; this makes neighbourhood filters countably generated, as required by the filter form of dominated convergence.

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

Each restricted cell is measurable (it is compact, hence closed).

theorem NRR.EMP.VariableBody.cellArea_eq_integral_indicator {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) : cellArea hA C s w i = ∫ (x : Geometry.Plane), (cellSet hA C s w i).indicator (fun (x : Geometry.Plane) => 1) x

Cell area as an indicator integral. The restricted cell area equals the Lebesgue integral of the 0/1 indicator of the cell.

theorem NRR.EMP.VariableBody.norm_cell_indicator_le_parent {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) (x : Geometry.Plane) : ‖(cellSet hA C s w i).indicator (fun (x : Geometry.Plane) => 1) x‖ ≤ K.carrier.indicator (fun (x : Geometry.Plane) => 1) x

The constant parent indicator dominates every cell indicator pointwise.

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

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

theorem NRR.EMP.VariableBody.continuous_cellArea_compactFamily {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] (sites : C(X, Config n)) (hA : 0 < A) (i : Fin n) : Continuous fun (z : BodySpace K A × X × (Fin n → ℝ)) => cellArea hA z.1 (sites z.2.1) z.2.2 i

Compact-family composition form. For a continuous site family sites : C(X, Config n), the restricted cell area is continuous jointly in the parent subbody, the base point x : X, and the weight vector. Only continuity of X is used; compactness is not required.