NRR.HalfSpaceCutArea — area of fixed-normal halfspace cuts

Defines lower and upper halfspace-cut areas for a planar convex body and proves their basic monotonicity and endpoint properties. The compatibility name cutArea denotes the lower cut area.

noncomputable def NRR.Geometry.ConvexBody.cutAreaLower (K : ConvexBody Plane) (u : Plane) (c : ℝ) : ℝ

Lower cut area: the real-valued Lebesgue measure of K ∩ {x | ⟪u, x⟫ ≤ c}.

Equations

• K.cutAreaLower u c = (MeasureTheory.volume (K.carrier ∩ NRR.Geometry.lowerClosedHalfspace u c)).toReal

noncomputable def NRR.Geometry.ConvexBody.cutAreaUpper (K : ConvexBody Plane) (u : Plane) (c : ℝ) : ℝ

Upper cut area: the real-valued Lebesgue measure of K ∩ {x | c ≤ ⟪u, x⟫}.

Equations

• K.cutAreaUpper u c = (MeasureTheory.volume (K.carrier ∩ NRR.Geometry.upperClosedHalfspace u c)).toReal

noncomputable def NRR.Geometry.ConvexBody.cutArea (K : ConvexBody Plane) (u : Plane) (c : ℝ) : ℝ

The compatibility name cutArea denotes the lower cut area.

Equations

• NRR.Geometry.ConvexBody.cutArea = NRR.Geometry.ConvexBody.cutAreaLower

Finiteness of the cut measures

theorem NRR.Geometry.ConvexBody.volume_inter_lowerClosedHalfspace_lt_top (K : ConvexBody Plane) (u : Plane) (c : ℝ) : MeasureTheory.volume (K.carrier ∩ lowerClosedHalfspace u c) < ⊤

theorem NRR.Geometry.ConvexBody.volume_inter_upperClosedHalfspace_lt_top (K : ConvexBody Plane) (u : Plane) (c : ℝ) : MeasureTheory.volume (K.carrier ∩ upperClosedHalfspace u c) < ⊤

Nonnegativity

theorem NRR.Geometry.ConvexBody.cutAreaLower_nonneg (K : ConvexBody Plane) (u : Plane) (c : ℝ) : 0 ≤ K.cutAreaLower u c

theorem NRR.Geometry.ConvexBody.cutAreaUpper_nonneg (K : ConvexBody Plane) (u : Plane) (c : ℝ) : 0 ≤ K.cutAreaUpper u c

Monotonicity in the threshold

theorem NRR.Geometry.ConvexBody.cutAreaLower_mono (K : ConvexBody Plane) (u : Plane) {a b : ℝ} (hab : a ≤ b) : K.cutAreaLower u a ≤ K.cutAreaLower u b

theorem NRR.Geometry.ConvexBody.cutAreaUpper_antitone (K : ConvexBody Plane) (u : Plane) {a b : ℝ} (hab : a ≤ b) : K.cutAreaUpper u b ≤ K.cutAreaUpper u a

Bounds by the total area

theorem NRR.Geometry.ConvexBody.cutAreaLower_le_area (K : ConvexBody Plane) (u : Plane) (c : ℝ) : K.cutAreaLower u c ≤ K.area

theorem NRR.Geometry.ConvexBody.cutAreaUpper_le_area (K : ConvexBody Plane) (u : Plane) (c : ℝ) : K.cutAreaUpper u c ≤ K.area