Sharpness of Grünbaum's centroid halfspace constant

This file constructs the full-dimensional standard simplex and its sharp centroid halfspace. It computes the relevant centroid coordinate by the layer-cake formula and proves that every universal project-level lower bound is at most grunbaumConstant.

@[reducible, inline]

abbrev Grunbaum.SimplexE (n : ℕ) : Type

Euclidean space in an arbitrary (possibly zero) dimension. The project type Euc d is definitionally SimplexE (d + 1).

Equations

• Grunbaum.SimplexE n = EuclideanSpace ℝ (Fin n)

noncomputable def Grunbaum.coordinateSum (n : ℕ) : SimplexE n →L[ℝ] ℝ

The sum of the coordinates, bundled as a continuous linear functional.

Equations

• Grunbaum.coordinateSum n = ∑ i : Fin n, EuclideanSpace.proj i

@[simp]

theorem Grunbaum.coordinateSum_apply (n : ℕ) (x : SimplexE n) : (coordinateSum n) x = ∑ i : Fin n, x.ofLp i

def Grunbaum.simplexSet (n : ℕ) : Set (SimplexE n)

The full-dimensional standard simplex xᵢ ≥ 0, ∑ xᵢ ≤ 1.

Equations

• Grunbaum.simplexSet n = {x : Grunbaum.SimplexE n | (∀ (i : Fin n), 0 ≤ x.ofLp i) ∧ (Grunbaum.coordinateSum n) x ≤ 1}

@[simp]

theorem Grunbaum.mem_simplexSet {n : ℕ} {x : SimplexE n} : x ∈ simplexSet n ↔ (∀ (i : Fin n), 0 ≤ x.ofLp i) ∧ (coordinateSum n) x ≤ 1

theorem Grunbaum.convex_simplexSet (n : ℕ) : Convex ℝ (simplexSet n)

theorem Grunbaum.isClosed_simplexSet (n : ℕ) : IsClosed (simplexSet n)

theorem Grunbaum.isCompact_simplexSet (n : ℕ) : IsCompact (simplexSet n)

theorem Grunbaum.nonempty_simplexSet (n : ℕ) : (simplexSet n).Nonempty

theorem Grunbaum.interior_simplexSet_nonempty (n : ℕ) : (interior (simplexSet n)).Nonempty

theorem Grunbaum.volume_simplexSet_pos (n : ℕ) : 0 < MeasureTheory.volume (simplexSet n)

theorem Grunbaum.volumeReal_simplexSet_pos (n : ℕ) : 0 < MeasureTheory.volume.real (simplexSet n)

def Grunbaum.simplexCap (n : ℕ) (t : ℝ) : Set (SimplexE n)

The part of the simplex below coordinate-sum level t.

Equations

• Grunbaum.simplexCap n t = Grunbaum.simplexSet n ∩ {x : Grunbaum.SimplexE n | (Grunbaum.coordinateSum n) x ≤ t}

theorem Grunbaum.simplexCap_eq_smul {n : ℕ} {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : simplexCap n t = t • simplexSet n

theorem Grunbaum.volumeReal_simplexCap {n : ℕ} {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : MeasureTheory.volume.real (simplexCap n t) = t ^ n * MeasureTheory.volume.real (simplexSet n)

theorem Grunbaum.restrictSimplex_tail {n : ℕ} {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : (MeasureTheory.volume.restrict (simplexSet n)).real {x : SimplexE n | t < (coordinateSum n) x} = (1 - t ^ n) * MeasureTheory.volume.real (simplexSet n)

The exact strict-tail measure of the coordinate sum on the simplex.

theorem Grunbaum.integral_coordinateSum (n : ℕ) : ∫ (x : SimplexE n) in simplexSet n, (coordinateSum n) x = ↑n / (↑n + 1) * MeasureTheory.volume.real (simplexSet n)

The first moment of the coordinate sum over the standard simplex.

noncomputable def Grunbaum.simplexCentroid (n : ℕ) : SimplexE n

The volume centroid of the standard simplex.

Equations

• Grunbaum.simplexCentroid n = ⨍ (x : Grunbaum.SimplexE n) in Grunbaum.simplexSet n, x

theorem Grunbaum.coordinateSum_simplexCentroid (n : ℕ) : (coordinateSum n) (simplexCentroid n) = ↑n / (↑n + 1)

The scalar coordinate needed to locate the sharp supporting hyperplane.

noncomputable def Grunbaum.sharpLevel (n : ℕ) : ℝ

The sharp normalized coordinate-sum threshold in dimension n.

Equations

• Grunbaum.sharpLevel n = ↑n / (↑n + 1)

def Grunbaum.sharpHalfspaceSet (n : ℕ) : Set (SimplexE n)

The simplex halfspace attaining the sharp Grünbaum fraction.

Equations

• Grunbaum.sharpHalfspaceSet n = {x : Grunbaum.SimplexE n | (Grunbaum.coordinateSum n) x ≤ Grunbaum.sharpLevel n}

theorem Grunbaum.sharpLevel_pos {n : ℕ} (hn : 0 < n) : 0 < sharpLevel n

theorem Grunbaum.sharpLevel_le_one (n : ℕ) : sharpLevel n ≤ 1

theorem Grunbaum.simplexCentroid_mem_sharpHalfspaceSet (n : ℕ) : simplexCentroid n ∈ sharpHalfspaceSet n

theorem Grunbaum.sharpHalfspaceSet_volume_ratio {n : ℕ} (hn : 0 < n) : MeasureTheory.volume.real (simplexSet n ∩ sharpHalfspaceSet n) / MeasureTheory.volume.real (simplexSet n) = sharpLevel n ^ n

def Grunbaum.simplexFullBody (d : ℕ) : FullDimensionalConvexBody d

The standard simplex, regarded as a full-dimensional body in project dimension d + 1.

Equations

• Grunbaum.simplexFullBody d = { carrier := Grunbaum.simplexSet (d + 1), convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

theorem Grunbaum.simplexFullBody_centroid (d : ℕ) : (simplexFullBody d).centroid = simplexCentroid (d + 1)

noncomputable def Grunbaum.sharpClosedHalfspace (d : ℕ) : ClosedHalfspace d

The sharp halfspace for the standard simplex.

Equations

• Grunbaum.sharpClosedHalfspace d = { normal := Grunbaum.coordinateSum (d + 1), threshold := Grunbaum.sharpLevel (d + 1), normal_ne_zero := ⋯ }

theorem Grunbaum.simplexFullBody_centroid_mem_sharpClosedHalfspace (d : ℕ) : (simplexFullBody d).centroid ∈ sharpClosedHalfspace d

theorem Grunbaum.sharpClosedHalfspace_ratio (d : ℕ) : halfspaceVolumeRatio (simplexFullBody d) (sharpClosedHalfspace d).normal (sharpClosedHalfspace d).threshold = grunbaumConstant d

def Grunbaum.IsUniversalCentroidHalfspaceLowerBound (d : ℕ) (c : ℝ) : Prop

c is a lower bound for every project convex body and every proper closed halfspace containing its centroid.

Equations

• One or more equations did not get rendered due to their size.

theorem Grunbaum.universalCentroidHalfspaceLowerBound_le_grunbaumConstant {d : ℕ} {c : ℝ} (hc : IsUniversalCentroidHalfspaceLowerBound d c) : c ≤ grunbaumConstant d

The simplex equality case shows that no universal centroid-halfspace lower bound can exceed grunbaumConstant d.