Grünbaum's centroid halfspace theorem

This file closes the geometric, measure-theoretic, and Jensen layers of the proof. The public theorem grunbaum_centroid_halfspace has only the assumptions in the mathematical statement.

theorem Grunbaum.truncDomain_eq_Ici_of_isMinOn {d : ℕ} {C : Set (Euc d)} {ℓ : Euc d →L[ℝ] ℝ} {x₀ : Euc d} (hx₀ : x₀ ∈ C) (hmin : IsMinOn (⇑ℓ) C x₀) : truncDomain C ℓ = Set.Ici (ℓ x₀)

theorem Grunbaum.cdf_map_uniformVolume_eq_truncVolumeRatio {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (⇑ℓ) (uniformVolume C))] : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (⇑ℓ) (uniformVolume C))) t = (MeasureTheory.volume (trunc C ℓ t) / MeasureTheory.volume C).toReal

theorem Grunbaum.cdfRoot_eq_cdf_rpow_map_uniformVolume {d : ℕ} (C : Set (Euc d)) (ℓ : Euc d →L[ℝ] ℝ) (t : ℝ) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (⇑ℓ) (uniformVolume C))] : cdfRoot C ℓ t = ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (⇑ℓ) (uniformVolume C))) t ^ (↑(d + 1))⁻¹

theorem Grunbaum.ae_map_uniformVolume_mem_Ici_of_isMinOn {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) {x₀ : Euc d} (hmin : IsMinOn (⇑ℓ) (↑C) x₀) : ∀ᵐ (t : ℝ) ∂MeasureTheory.Measure.map (⇑ℓ) (uniformVolume ↑C), t ∈ Set.Ici (ℓ x₀)

theorem Grunbaum.integrable_id_map_uniformVolume {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => t) (MeasureTheory.Measure.map (⇑ℓ) (uniformVolume ↑C))

theorem Grunbaum.cdfRoot_centroid_lower_bound {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) (hℓ : ℓ ≠ 0) : ↑(d + 1) / ↑(d + 2) ≤ cdfRoot (↑C) ℓ (ℓ C.centroid)

theorem Grunbaum.grunbaum_centroid_halfspace_functional {d : ℕ} (C : FullDimensionalConvexBody d) (ℓ : Euc d →L[ℝ] ℝ) (hℓ : ℓ ≠ 0) (a : ℝ) (ha : ℓ C.centroid ≤ a) : grunbaumConstant d ≤ halfspaceVolumeRatio C ℓ a

The functional form of Grünbaum's centroid halfspace theorem in positive dimension n = d + 1.

theorem Grunbaum.grunbaum_centroid_halfspace {d : ℕ} (C : FullDimensionalConvexBody d) (H : ClosedHalfspace d) (hcentroid : C.centroid ∈ H) : grunbaumConstant d ≤ halfspaceVolumeRatio C H.normal H.threshold

Grünbaum's centroid halfspace theorem. Every proper closed halfspace containing the centroid of a full-dimensional convex body in dimension d + 1 contains at least ((d + 1) / (d + 2)) ^ (d + 1) of its volume.