The full-dimensional model of the standard simplex

The standard simplex on Option ι naturally lives in the affine hyperplane whose coordinates sum to one. For measure-theoretic arguments it is more convenient to delete the coordinate indexed by none. The resulting full-dimensional simplex consists of the nonnegative vectors whose coordinate sum is at most one; the deleted coordinate is 1 - ∑ i, x i.

This file records the elementary geometry needed to state the simplex halfspace argument: the simplex, its centroid, and the value at that centroid of the linear functional determined by a coefficient vector.

def Feige.fullSimplex (ι : Type u_2) [Fintype ι] : Set (ι → ℝ)

The full-dimensional standard simplex in ι → ℝ, obtained by deleting one coordinate from the standard simplex on Option ι.

Equations

• Feige.fullSimplex ι = {x : ι → ℝ | (∀ (i : ι), 0 ≤ x i) ∧ ∑ i : ι, x i ≤ 1}

theorem Feige.mem_fullSimplex_iff {ι : Type u_1} [Fintype ι] {x : ι → ℝ} : x ∈ fullSimplex ι ↔ (∀ (i : ι), 0 ≤ x i) ∧ ∑ i : ι, x i ≤ 1

theorem Feige.convex_fullSimplex {ι : Type u_1} [Fintype ι] : Convex ℝ (fullSimplex ι)

theorem Feige.isClosed_fullSimplex {ι : Type u_1} [Fintype ι] : IsClosed (fullSimplex ι)

theorem Feige.fullSimplex_subset_Icc {ι : Type u_1} [Fintype ι] : fullSimplex ι ⊆ Set.Icc 0 1

theorem Feige.isCompact_fullSimplex {ι : Type u_1} [Fintype ι] : IsCompact (fullSimplex ι)

theorem Feige.measurableSet_fullSimplex {ι : Type u_1} [Fintype ι] : MeasurableSet (fullSimplex ι)

theorem Feige.volume_fullSimplex_lt_top {ι : Type u_1} [Fintype ι] : MeasureTheory.volume (fullSimplex ι) < ⊤

noncomputable def Feige.simplexCentroid (ι : Type u_2) [Fintype ι] : ι → ℝ

The centroid of the full-dimensional standard simplex. Its ι coordinates, as well as the deleted coordinate, all equal 1 / (card ι + 1).

Equations

• Feige.simplexCentroid ι x✝ = (↑(Fintype.card ι) + 1)⁻¹

@[simp]

theorem Feige.simplexCentroid_apply {ι : Type u_1} [Fintype ι] (i : ι) : simplexCentroid ι i = (↑(Fintype.card ι) + 1)⁻¹

theorem Feige.sum_simplexCentroid {ι : Type u_1} [Fintype ι] : ∑ i : ι, simplexCentroid ι i = ↑(Fintype.card ι) / (↑(Fintype.card ι) + 1)

theorem Feige.simplexCentroid_mem_fullSimplex {ι : Type u_1} [Fintype ι] : simplexCentroid ι ∈ fullSimplex ι

theorem Feige.Icc_zero_centroid_subset_fullSimplex {ι : Type u_1} [Fintype ι] : Set.Icc 0 (simplexCentroid ι) ⊆ fullSimplex ι

The coordinate box from zero to the centroid is contained in the simplex. It supplies a simple positive-volume subset without requiring the exact volume formula for a simplex.

theorem Feige.volume_fullSimplex_pos {ι : Type u_1} [Fintype ι] : 0 < MeasureTheory.volume (fullSimplex ι)

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

The linear functional cutting out the simplex halfspace associated to the coefficient vector y.

Equations

• Feige.simplexLinearForm y x = ∑ i : ι, y i * x i

theorem Feige.simplexLinearForm_apply {ι : Type u_1} [Fintype ι] (y x : ι → ℝ) : simplexLinearForm y x = ∑ i : ι, y i * x i

theorem Feige.simplexLinearForm_centroid {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : simplexLinearForm y (simplexCentroid ι) = (∑ i : ι, y i) / (↑(Fintype.card ι) + 1)

Evaluation of L_y at the centroid.

theorem Feige.one_le_simplexLinearForm_centroid {ι : Type u_1} [Fintype ι] (y : ι → ℝ) (hy : ↑(Fintype.card ι) + 1 ≤ ∑ i : ι, y i) : 1 ≤ simplexLinearForm y (simplexCentroid ι)

In the δ = 1 normalization used in §2.2, ∑ i, y i ≥ card ι + 1 means that the centroid lies in the upper halfspace 1 ≤ L_y.