Uniform measure and halfspace statistic on the simplex

This file equips the full-dimensional simplex with normalized Lebesgue measure. It also isolates the α = 0 centroid-halfspace statement used in the δ = 1 specialization of §2.2. Everything after that geometric input, including the strict-boundary/complement step, is proved here.

noncomputable def Feige.simplexRestrictedVolume (ι : Type u_2) [Fintype ι] : MeasureTheory.Measure (ι → ℝ)

Lebesgue measure restricted to the full-dimensional simplex.

Equations

• Feige.simplexRestrictedVolume ι = MeasureTheory.volume.restrict (Feige.fullSimplex ι)

noncomputable def Feige.simplexUniformMeasure (ι : Type u_2) [Fintype ι] : MeasureTheory.Measure (ι → ℝ)

Uniform probability measure on the full-dimensional standard simplex.

Equations

• Feige.simplexUniformMeasure ι = (MeasureTheory.volume (Feige.fullSimplex ι))⁻¹ • Feige.simplexRestrictedVolume ι

instance Feige.simplexUniformMeasure.isProbabilityMeasure {ι : Type u_1} [Fintype ι] : MeasureTheory.IsProbabilityMeasure (simplexUniformMeasure ι)

theorem Feige.simplexUniformMeasure_apply {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : MeasurableSet s) : (simplexUniformMeasure ι) s = (MeasureTheory.volume (fullSimplex ι))⁻¹ * MeasureTheory.volume (s ∩ fullSimplex ι)

noncomputable def Feige.simplexK {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : ℝ

The simplex form of the Dirichlet statistic Kₙ in (2.1).

Equations

• Feige.simplexK y = (Feige.simplexUniformMeasure ι).real {x : ι → ℝ | Feige.simplexLinearForm y x ≤ 1}

theorem Feige.measurableSet_simplexK_event {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : MeasurableSet {x : ι → ℝ | simplexLinearForm y x ≤ 1}

theorem Feige.simplexK_nonneg {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : 0 ≤ simplexK y

theorem Feige.simplexK_le_one {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : simplexK y ≤ 1

def Feige.SimplexCentroidHalfspaceProperty {ι : Type u_1} [Fintype ι] : Prop

The precise α = 0 simplex centroid-halfspace conclusion used by the δ = 1 geometric estimate in §2.2.

Equations

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

theorem Feige.simplex_upper_compl {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : {x : ι → ℝ | 1 < simplexLinearForm y x}ᶜ = {x : ι → ℝ | simplexLinearForm y x ≤ 1}

The strict upper halfspace and the closed sublevel event are complements.

theorem Feige.simplex_largeSumBridge {ι : Type u_1} [Fintype ι] (hcentroid : SimplexCentroidHalfspaceProperty) (y : ι → ℝ) : (∀ (i : ι), 0 ≤ y i) → ↑(Fintype.card ι) + 1 ≤ ∑ i : ι, y i → simplexK y ≤ 1 - sharpConstant (Fintype.card ι)

Specialized Grünbaum immediately gives the deterministic large-sum bridge for the simplex statistic.