Definitions for Grünbaum's centroid halfspace theorem

Mathlib's ConvexBody permits lower-dimensional compact convex sets. In finite-dimensional convex geometry, a convex body is normally required to have nonempty interior. FullDimensionalConvexBody records precisely that standard convention.

@[reducible, inline]

abbrev Grunbaum.Euc (d : ℕ) : Type

Euclidean space of positive dimension d + 1.

Equations

• Grunbaum.Euc d = EuclideanSpace ℝ (Fin (d + 1))

structure Grunbaum.FullDimensionalConvexBody (d : ℕ) : Type

A compact convex set with nonempty interior.

• carrier : Set (Euc d)

  The underlying point set.

• convex' : Convex ℝ self.carrier

  Convexity of the body.

• isCompact' : IsCompact self.carrier

  Compactness of the body.

• interior_nonempty' : (interior self.carrier).Nonempty

  The body is full-dimensional.

@[instance_reducible]

instance Grunbaum.FullDimensionalConvexBody.instSetLikeEuc {d : ℕ} : SetLike (FullDimensionalConvexBody d) (Euc d)

Equations

• Grunbaum.FullDimensionalConvexBody.instSetLikeEuc = { coe := Grunbaum.FullDimensionalConvexBody.carrier, coe_injective := ⋯ }

theorem Grunbaum.FullDimensionalConvexBody.convex {d : ℕ} (C : FullDimensionalConvexBody d) : Convex ℝ ↑C

theorem Grunbaum.FullDimensionalConvexBody.isCompact {d : ℕ} (C : FullDimensionalConvexBody d) : IsCompact ↑C

theorem Grunbaum.FullDimensionalConvexBody.isClosed {d : ℕ} (C : FullDimensionalConvexBody d) : IsClosed ↑C

theorem Grunbaum.FullDimensionalConvexBody.interior_nonempty {d : ℕ} (C : FullDimensionalConvexBody d) : (interior ↑C).Nonempty

theorem Grunbaum.FullDimensionalConvexBody.nonempty {d : ℕ} (C : FullDimensionalConvexBody d) : (↑C).Nonempty

theorem Grunbaum.FullDimensionalConvexBody.volume_pos {d : ℕ} (C : FullDimensionalConvexBody d) : 0 < MeasureTheory.volume ↑C

theorem Grunbaum.FullDimensionalConvexBody.volume_ne_zero {d : ℕ} (C : FullDimensionalConvexBody d) : MeasureTheory.volume ↑C ≠ 0

theorem Grunbaum.FullDimensionalConvexBody.volume_ne_top {d : ℕ} (C : FullDimensionalConvexBody d) : MeasureTheory.volume ↑C ≠ ⊤

noncomputable def Grunbaum.FullDimensionalConvexBody.centroid {d : ℕ} (C : FullDimensionalConvexBody d) : Euc d

The volume centroid of a full-dimensional convex body.

Equations

• C.centroid = ⨍ (x : Grunbaum.Euc d) in ↑C, x

def Grunbaum.closedHalfspace {d : ℕ} (ℓ : Euc d →L[ℝ] ℝ) (a : ℝ) : Set (Euc d)

The closed halfspace cut out by ℓ x ≤ a.

Equations

• Grunbaum.closedHalfspace ℓ a = ⇑ℓ ⁻¹' Set.Iic a

structure Grunbaum.ClosedHalfspace (d : ℕ) : Type

A (proper) closed halfspace, represented by a nonzero continuous linear functional and a threshold.

• normal : Euc d →L[ℝ] ℝ

  The defining normal functional.

• threshold : ℝ

  The defining threshold.

• normal_ne_zero : self.normal ≠ 0

  A halfspace has a nonzero normal.

@[instance_reducible]

instance Grunbaum.ClosedHalfspace.instCoeSetEuc {d : ℕ} : Coe (ClosedHalfspace d) (Set (Euc d))

Equations

• Grunbaum.ClosedHalfspace.instCoeSetEuc = { coe := fun (H : Grunbaum.ClosedHalfspace d) => Grunbaum.closedHalfspace H.normal H.threshold }

@[instance_reducible]

instance Grunbaum.ClosedHalfspace.instMembershipEuc {d : ℕ} : Membership (Euc d) (ClosedHalfspace d)

Equations

• Grunbaum.ClosedHalfspace.instMembershipEuc = { mem := fun (H : Grunbaum.ClosedHalfspace d) (x : Grunbaum.Euc d) => x ∈ Grunbaum.closedHalfspace H.normal H.threshold }

@[simp]

theorem Grunbaum.ClosedHalfspace.mem_iff {d : ℕ} {x : Euc d} {H : ClosedHalfspace d} : x ∈ H ↔ H.normal x ≤ H.threshold

theorem Grunbaum.ClosedHalfspace.isClosed {d : ℕ} (H : ClosedHalfspace d) : IsClosed (closedHalfspace H.normal H.threshold)

noncomputable def Grunbaum.halfspaceVolumeRatio {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) (a : ℝ) : ℝ

The normalized volume of a body's intersection with a closed halfspace.

Equations

• Grunbaum.halfspaceVolumeRatio C ℓ a = (MeasureTheory.volume (↑C ∩ Grunbaum.closedHalfspace ℓ a) / MeasureTheory.volume ↑C).toReal

noncomputable def Grunbaum.grunbaumConstant (d : ℕ) : ℝ

The sharp constant (n / (n + 1)) ^ n in dimension n = d + 1.

Equations

• Grunbaum.grunbaumConstant d = (↑(d + 1) / ↑(d + 2)) ^ (d + 1)