Boundary nullity for compact convex subbodies

The frontier of a convex set in a finite-dimensional real normed space is Lebesgue-null. On the plane this applies uniformly to every NRR.ConvexSubbody, including lower-dimensional (degenerate) ones, since the underlying Mathlib convex body is convex.

The a.e. complement statement ConvexSubbody.ae_not_mem_frontier is the exact exceptional-set lemma required by membership stability and area continuity: almost every point of the plane avoids the frontier of a given subbody.

theorem NRR.ConvexSubbody.frontier_null {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : MeasureTheory.volume (frontier ↑C.body) = 0

The frontier of a convex subbody carrier is Lebesgue-null. This holds for arbitrary subbodies, including lower-dimensional ones, via Convex.addHaar_frontier.

theorem NRR.ConvexSubbody.ae_not_mem_frontier {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ∀ᵐ (x : Geometry.Plane), x ∉ frontier ↑C.body

Almost every point of the plane lies outside the frontier of a convex subbody. This is the exceptional-set lemma consumed by dominated-convergence arguments for membership and area continuity.

theorem NRR.mathlibConvexBody_frontier_null (C : ConvexBody Geometry.Plane) : MeasureTheory.volume (frontier ↑C) = 0

Root-body form: the frontier of any Mathlib ConvexBody Plane is Lebesgue-null.