From truncation concavity to the Grünbaum volume bound

theorem Grunbaum.trunc_mono {d : ℕ} {C : Set (Euc d)} {ℓ : Euc d →L[ℝ] ℝ} {s t : ℝ} (hst : s ≤ t) : trunc C ℓ s ⊆ trunc C ℓ t

theorem Grunbaum.cdfRoot_pow_dimension {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) : cdfRoot C ℓ t ^ (d + 1) = (MeasureTheory.volume (trunc C ℓ t) / MeasureTheory.volume C).toReal

theorem Grunbaum.truncVolumeRatio_mono {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) {s t : ℝ} (hst : s ≤ t) : (MeasureTheory.volume (trunc (↑C) ℓ s) / MeasureTheory.volume ↑C).toReal ≤ (MeasureTheory.volume (trunc (↑C) ℓ t) / MeasureTheory.volume ↑C).toReal

theorem Grunbaum.grunbaum_bound_of_cdfRoot {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) (a : ℝ) (hcentroid : ℓ C.centroid ≤ a) (hroot : ↑(d + 1) / ↑(d + 2) ≤ cdfRoot (↑C) ℓ (ℓ C.centroid)) : grunbaumConstant d ≤ halfspaceVolumeRatio C ℓ a

Raise a lower bound on the CDF root at the centroid and enlarge the centroid cut to any containing halfspace.