NRR.Geometry.HalfspaceFiniteIntersectionAreaContinuity

Area continuity for finite intersections of fixed-normal moving halfspaces.

For a finite index type ι, fixed normals u : ι → Plane and offsets c : ι → ℝ, the set finiteHalfspaceIntersection K u c is the intersection of a planar convex body K with the finitely many closed lower halfspaces {x | ⟪u i, x⟫ ≤ c i}, kept purely as a Set Plane (never bundled as a ConvexBody). Its real-valued Lebesgue area is finiteHalfspaceIntersectionArea K u c.

The main result continuous_finiteHalfspaceIntersectionArea states that this area depends continuously on continuously-moving offsets.

The nondegeneracy hypothesis ∀ i, u i ≠ 0 is necessary

Just as in the single-halfspace case (continuous_cutAreaLower_fixedNormal), the hypothesis u i ≠ 0 for each i is mathematically required, and its absence would make the theorem false. Indeed, if some u i = 0 then lowerClosedHalfspace 0 (c i) = {x | 0 ≤ c i}, which is the whole plane for c i ≥ 0 and empty for c i < 0. Taking a single index with u 0 = 0 and offset c a 0 = a, the intersection area jumps from 0 (for a < 0) to K.area > 0 (for a ≥ 0) at a = 0, hence is discontinuous. The corresponding "boundary slice" {x | ⟪0, x⟫ = 0} is the whole plane, which is not null, so the boundary-null argument breaks down exactly where the result fails. We therefore keep ∀ i, u i ≠ 0 explicit; this is how the degenerate normal is handled rather than omitted.

Proof route

The offset-to-area map factors as A ∘ c where A : (ι → ℝ) → ℝ, A f = finiteHalfspaceIntersectionArea K u f. Since ι is finite, ι → ℝ is a (first-countable, metrizable) product space, so Continuous A follows from MeasureTheory.continuous_of_dominated:

• the area is the integral of the indicator of the (measurable, K-contained) intersection;
• the integrands are dominated by the integrable indicator 1_K (finite, K compact);
• for a.e. x, the map f ↦ 1_{∀ i, ⟪u i, x⟫ ≤ f i} is continuous (in fact locally constant) at any f₀ — it can fail only on the finite union of boundary hyperplanes ⋃ i {x | ⟪u i, x⟫ = f₀ i}, which is null because each u i ≠ 0.

Continuity for an arbitrary topological domain α is then obtained by composing with the continuous offset map c : α → ι → ℝ, so no first-countability hypothesis on α is needed.

def NRR.Geometry.ConvexBody.finiteHalfspaceIntersection {ι : Type u_1} (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) : Set Plane

The intersection of a convex body K with the finitely many closed lower halfspaces with normals u i and offsets c i. Kept purely as a Set Plane.

Equations

• K.finiteHalfspaceIntersection u c = K.carrier ∩ ⋂ (i : ι), NRR.Geometry.lowerClosedHalfspace (u i) (c i)

noncomputable def NRR.Geometry.ConvexBody.finiteHalfspaceIntersectionArea {ι : Type u_1} (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) : ℝ

The real-valued Lebesgue area of a finite fixed-normal halfspace intersection.

Equations

• K.finiteHalfspaceIntersectionArea u c = (MeasureTheory.volume (K.finiteHalfspaceIntersection u c)).toReal

theorem NRR.Geometry.ConvexBody.finiteHalfspaceIntersection_subset {ι : Type u_1} (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) : K.finiteHalfspaceIntersection u c ⊆ K.carrier

A finite halfspace intersection is contained in the body.

theorem NRR.Geometry.ConvexBody.mem_finiteHalfspaceIntersection {ι : Type u_1} (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) (x : Plane) : x ∈ K.finiteHalfspaceIntersection u c ↔ x ∈ K.carrier ∧ ∀ (i : ι), inner ℝ (u i) x ≤ c i

Membership in a finite halfspace intersection.

theorem NRR.Geometry.ConvexBody.measurableSet_finiteHalfspaceIntersection {ι : Type u_1} [Countable ι] (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) : MeasurableSet (K.finiteHalfspaceIntersection u c)

A finite halfspace intersection is measurable.

theorem NRR.Geometry.ConvexBody.volume_finiteHalfspaceIntersection_lt_top {ι : Type u_1} (K : ConvexBody Plane) (u : ι → Plane) (c : ι → ℝ) : MeasureTheory.volume (K.finiteHalfspaceIntersection u c) < ⊤

The measure of a finite halfspace intersection is finite.

theorem NRR.Geometry.ConvexBody.continuous_finiteHalfspaceIntersectionArea_pi {ι : Type u_1} [Finite ι] (K : ConvexBody Plane) (u : ι → Plane) (hu : ∀ (i : ι), u i ≠ 0) : Continuous fun (f : ι → ℝ) => K.finiteHalfspaceIntersectionArea u f

theorem NRR.Geometry.ConvexBody.continuous_finiteHalfspaceIntersectionArea {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] [Finite ι] (K : ConvexBody Plane) (u : ι → Plane) (hu : ∀ (i : ι), u i ≠ 0) (c : α → ι → ℝ) (hc : Continuous c) : Continuous fun (a : α) => K.finiteHalfspaceIntersectionArea u (c a)

Continuity of the finite fixed-normal moving-halfspace intersection area. For fixed nonzero normals u and continuously-moving offsets c a, the intersection area depends continuously on a. The hypothesis ∀ i, u i ≠ 0 is necessary (see the module docstring).

theorem NRR.Geometry.ConvexBody.continuous_finiteHalfspaceIntersectionArea_weights {m n : ℕ} (K : ConvexBody Plane) (u : Fin m → Plane) (hu : ∀ (i : Fin m), u i ≠ 0) (c : (Fin n → ℝ) → Fin m → ℝ) (hc : Continuous c) : Continuous fun (w : Fin n → ℝ) => K.finiteHalfspaceIntersectionArea u (c w)

Fallback / power-cell specialization. Weights w : Fin n → ℝ moving the offsets of m fixed-normal halfspaces yield a continuous restricted-intersection area.