NRR.HalfSpaceCutAreaContinuity — continuity of fixed-normal cut areas

For a fixed nonzero normal direction u, this module proves that the real-valued cut-area functionals cutAreaLower K u · and cutAreaUpper K u · (defined in NRR.HalfSpaceCutArea) are continuous functions of the threshold c : ℝ.

The nondegeneracy hypothesis u ≠ 0 is necessary

The hypothesis u ≠ 0 is not a technical convenience — it is mathematically required. When u = 0 we have ⟪0, x⟫ = 0 for every x, so lowerClosedHalfspace 0 c = {x | 0 ≤ c}, which equals ∅ for c < 0 and the whole plane for c ≥ 0. Hence cutAreaLower K 0 c is the step function that jumps from 0 to K.area at c = 0; since a solid convex body has strictly positive area, this function is genuinely discontinuous at c = 0. (Equivalently: the "boundary slice" {x | ⟪0, x⟫ = c} at c = 0 is the whole plane, which is not null, so the boundary-null argument below breaks down exactly where the result fails.) Stating the theorems without u ≠ 0 would therefore be stating a false proposition, so the hypothesis is kept explicit. This is how the u = 0 case is handled rather than omitted.

Proof route

The cut area is written as an integral of an indicator, cutAreaLower K u c = ∫ x, ((K : Set Plane) ∩ lowerClosedHalfspace u c).indicator (fun _ => 1) x, and continuity in c follows from MeasureTheory.continuousAt_of_dominated:

• the integrands are dominated by the integrable indicator 1_K (finite because K is compact);
• for a.e. x, the map c ↦ 1_{⟪u,x⟫ ≤ c} is continuous at any point c₀ — it fails only on the slice {x ∈ K | ⟪u, x⟫ = c₀}, which is null by lowerCut_boundary_null (needs u ≠ 0).

theorem NRR.Geometry.ConvexBody.lowerCut_boundary_null (K : ConvexBody Plane) {u : Plane} (hu : u ≠ 0) (c : ℝ) : MeasureTheory.volume (K.carrier ∩ {x : Plane | inner ℝ u x = c}) = 0

The boundary slice K ∩ {x | ⟪u, x⟫ = c} of a fixed-normal cut has Lebesgue measure zero, provided the normal u is nonzero. Derived from NRR.Halfspace.hyperplane_null.

theorem NRR.Geometry.ConvexBody.continuous_cutAreaLower_fixedNormal (K : ConvexBody Plane) (u : Plane) (hu : u ≠ 0) : Continuous fun (c : ℝ) => K.cutAreaLower u c

Continuity of the lower fixed-normal cut area in the threshold, for a nonzero normal.

theorem NRR.Geometry.ConvexBody.continuous_cutAreaUpper_fixedNormal (K : ConvexBody Plane) (u : Plane) (hu : u ≠ 0) : Continuous fun (c : ℝ) => K.cutAreaUpper u c

Continuity of the upper fixed-normal cut area in the threshold, for a nonzero normal.