NRR.Geometry.ConvexBody — cutting a convex body by a closed halfspace

This module provides a reusable API for intersecting a solid ConvexBody with a closed halfspace determined by a normal vector u and a threshold t. It is a core primitive for cutting convex bodies by hyperplanes and building partitions.

Setup

E is a real inner product space. For a normal vector u : E and threshold t : ℝ we define the two closed halfspaces

• lowerClosedHalfspace u t = {x | inner ℝ u x ≤ t};
• upperClosedHalfspace u t = {x | t ≤ inner ℝ u x}.

Each is convex (from linearity of the inner product) and closed (as the sublevel/superlevel set of a continuous functional).

Cuts

Intersecting a convex body K with a closed halfspace always yields a compact convex set (a closed subset of the compact K, and an intersection of convex sets). It is again a solid ConvexBody only when its interior is nonempty, so the constructors

• ConvexBody.cutLowerClosed K u t hInt
• ConvexBody.cutUpperClosed K u t hInt

require the nonempty-interior hypothesis hInt explicitly. We do not claim the cut is a ConvexBody unconditionally, and we do not introduce an axiom for the nonempty interior.

Halfspace definitions are local

There is no oriented-hyperplane file over a general inner product space in the library yet (the plane-specific NRR.Halfspace lives in a different, E2-specific development), so the halfspace definitions are kept minimal here; downstream modules may generalize them.

Note on inner

In the current Mathlib the real inner product is written inner ℝ u x (the scalar field is an explicit argument), which is what appears throughout this file.

Import policy

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here.

Closed halfspaces

def NRR.Geometry.lowerClosedHalfspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : Set E

The closed lower halfspace with normal u and threshold t: {x | inner ℝ u x ≤ t}.

Equations

• NRR.Geometry.lowerClosedHalfspace u t = {x : E | inner ℝ u x ≤ t}

def NRR.Geometry.upperClosedHalfspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : Set E

The closed upper halfspace with normal u and threshold t: {x | t ≤ inner ℝ u x}.

Equations

• NRR.Geometry.upperClosedHalfspace u t = {x : E | t ≤ inner ℝ u x}

@[simp]

theorem NRR.Geometry.mem_lowerClosedHalfspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) (x : E) : x ∈ lowerClosedHalfspace u t ↔ inner ℝ u x ≤ t

@[simp]

theorem NRR.Geometry.mem_upperClosedHalfspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) (x : E) : x ∈ upperClosedHalfspace u t ↔ t ≤ inner ℝ u x

theorem NRR.Geometry.lowerClosedHalfspace_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : Convex ℝ (lowerClosedHalfspace u t)

theorem NRR.Geometry.upperClosedHalfspace_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : Convex ℝ (upperClosedHalfspace u t)

theorem NRR.Geometry.lowerClosedHalfspace_isClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : IsClosed (lowerClosedHalfspace u t)

theorem NRR.Geometry.upperClosedHalfspace_isClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : E) (t : ℝ) : IsClosed (upperClosedHalfspace u t)

Compactness of the intersection

theorem NRR.Geometry.ConvexBody.inter_lowerClosedHalfspace_isCompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) : IsCompact (K.carrier ∩ lowerClosedHalfspace u t)

theorem NRR.Geometry.ConvexBody.inter_upperClosedHalfspace_isCompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) : IsCompact (K.carrier ∩ upperClosedHalfspace u t)

The cuts

def NRR.Geometry.ConvexBody.cutLowerClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ lowerClosedHalfspace u t)).Nonempty) : ConvexBody E

The cut of a convex body K by the closed lower halfspace {x | inner ℝ u x ≤ t}, as a ConvexBody. Solidity is not automatic, so the nonempty-interior hypothesis hInt is required explicitly.

Equations

• K.cutLowerClosed u t hInt = { carrier := K.carrier ∩ NRR.Geometry.lowerClosedHalfspace u t, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := hInt }

def NRR.Geometry.ConvexBody.cutUpperClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ upperClosedHalfspace u t)).Nonempty) : ConvexBody E

The cut of a convex body K by the closed upper halfspace {x | t ≤ inner ℝ u x}, as a ConvexBody. Solidity is not automatic, so the nonempty-interior hypothesis hInt is required explicitly.

Equations

• K.cutUpperClosed u t hInt = { carrier := K.carrier ∩ NRR.Geometry.upperClosedHalfspace u t, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := hInt }

@[simp]

theorem NRR.Geometry.ConvexBody.cutLowerClosed_carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ lowerClosedHalfspace u t)).Nonempty) : (K.cutLowerClosed u t hInt).carrier = K.carrier ∩ lowerClosedHalfspace u t

@[simp]

theorem NRR.Geometry.ConvexBody.cutUpperClosed_carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ upperClosedHalfspace u t)).Nonempty) : (K.cutUpperClosed u t hInt).carrier = K.carrier ∩ upperClosedHalfspace u t

theorem NRR.Geometry.ConvexBody.mem_cutLowerClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ lowerClosedHalfspace u t)).Nonempty) (x : E) : x ∈ (K.cutLowerClosed u t hInt).carrier ↔ x ∈ K.carrier ∧ inner ℝ u x ≤ t

theorem NRR.Geometry.ConvexBody.mem_cutUpperClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) (u : E) (t : ℝ) (hInt : (interior (K.carrier ∩ upperClosedHalfspace u t)).Nonempty) (x : E) : x ∈ (K.cutUpperClosed u t hInt).carrier ↔ x ∈ K.carrier ∧ t ≤ inner ℝ u x