NRR.EMP.VariableBody.IndicatorStability — a.e. stability of cell indicators

For a variable planar body C : BodySpace K A, a configuration s : Config n, and weights w : Fin n → ℝ, the restricted power cell of site i is the parent body intersected with finitely many closed lower halfspaces. When the body, sites, and weights tend to a limit along an arbitrary filter, the 0/1 indicator of the restricted cell converges pointwise almost everywhere to the indicator of the limiting cell.

The exceptional null set is explicit:

frontier(C₀)
∪ ⋃ j : {j // j ≠ i},
    {x | ⟪sepNormal s₀ i j, x⟫ = sepOffset s₀ w₀ i j}

The parent frontier is Lebesgue-null (ConvexSubbody.frontier_null), and every off-diagonal wall is Lebesgue-null because the separating normal is nonzero (sepNormal_ne_zero, NRR.Halfspace.hyperplane_null). Outside this set the point avoids the limiting parent frontier, so BodySpace.eventually_mem_iff_of_not_mem_frontier controls the parent membership, and each off-diagonal scalar ⟪sepNormal (s a) i j, x⟫ - sepOffset (s a) (w a) i j tends to a nonzero limit, hence has eventually constant sign. Combining finitely many eventual statements and rewriting membership through cellSet_eq_offDiag_halfspaces gives eventual membership equivalence, which converts to convergence of the indicator.

This module uses no compactness of Config n and no continuity of the normalized weight; it is an input to area continuity, not the reverse.

theorem NRR.EMP.VariableBody.eventually_cell_membership_eq_of_goodPoint {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) {α : Type u_1} {l : Filter α} {C : α → BodySpace K A} {C₀ : BodySpace K A} {s : α → Config n} {s₀ : Config n} {w : α → Fin n → ℝ} {w₀ : Fin n → ℝ} (hC : Filter.Tendsto C l (nhds C₀)) (hs : Filter.Tendsto s l (nhds s₀)) (hw : Filter.Tendsto w l (nhds w₀)) (i : Fin n) (x : Geometry.Plane) (hxParent : x ∉ frontier ↑C₀.body.body) (hxWalls : ∀ (j : { j : Fin n // j ≠ i }), inner ℝ (sepNormal s₀ i ↑j) x ≠ sepOffset s₀ w₀ i ↑j) : ∀ᶠ (a : α) in l, x ∈ cellSet hA (C a) (s a) (w a) i ↔ x ∈ cellSet hA C₀ s₀ w₀ i

Eventual membership equivalence at a good point. If x avoids the frontier of the limiting parent body and all limiting off-diagonal walls, then eventually along the filter, membership of x in the moving cell agrees with membership in the limiting cell.

theorem NRR.EMP.VariableBody.tendsto_cell_indicator_ae {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) {α : Type u_1} {l : Filter α} {C : α → BodySpace K A} {C₀ : BodySpace K A} {s : α → Config n} {s₀ : Config n} {w : α → Fin n → ℝ} {w₀ : Fin n → ℝ} (hC : Filter.Tendsto C l (nhds C₀)) (hs : Filter.Tendsto s l (nhds s₀)) (hw : Filter.Tendsto w l (nhds w₀)) (i : Fin n) : ∀ᵐ (x : Geometry.Plane), Filter.Tendsto (fun (a : α) => (cellSet hA (C a) (s a) (w a) i).indicator (fun (x : Geometry.Plane) => 1) x) l (nhds ((cellSet hA C₀ s₀ w₀ i).indicator (fun (x : Geometry.Plane) => 1) x))

Almost-everywhere stability of the cell indicator. As the body, sites, and weights tend to a limit along an arbitrary filter, the 0/1 indicator of the restricted power cell of site i converges pointwise almost everywhere to the indicator of the limiting cell.