Weighted halfspaces on the Euclidean standard simplex

This file aligns the weighted linear form used in Feige's simplex argument with the positive-dimensional Euclidean model used by the Grünbaum formalization.

noncomputable def Feige.euclideanSimplexLinearForm {n : ℕ} (y : Fin n → ℝ) : Grunbaum.SimplexE n →L[ℝ] ℝ

The weighted coordinate functional on Mathlib's Euclidean-space model.

Equations

• Feige.euclideanSimplexLinearForm y = ∑ i : Fin n, y i • EuclideanSpace.proj i

@[simp]

theorem Feige.euclideanSimplexLinearForm_apply {n : ℕ} (y : Fin n → ℝ) (x : Grunbaum.SimplexE n) : (euclideanSimplexLinearForm y) x = ∑ i : Fin n, y i * x.ofLp i

theorem Feige.euclideanSimplexLinearForm_comp_simplexToEuclidean {n : ℕ} (y x : Fin n → ℝ) : (euclideanSimplexLinearForm y) (simplexToEuclidean n x) = simplexLinearForm y x

theorem Feige.euclideanSimplexLinearForm_ne_zero_of_sum_pos {n : ℕ} {y : Fin n → ℝ} (hy : 0 < ∑ i : Fin n, y i) : euclideanSimplexLinearForm y ≠ 0

theorem Feige.euclideanSimplexLinearForm_centroid {n : ℕ} (y : Fin n → ℝ) : (euclideanSimplexLinearForm y) (Grunbaum.simplexCentroid n) = (∑ i : Fin n, y i) / (↑n + 1)

The weighted form evaluated at the standard-simplex volume centroid.

theorem Feige.one_le_euclideanSimplexLinearForm_centroid {d : ℕ} (y : Fin (d + 1) → ℝ) (hsum : ↑(d + 1) + 1 ≤ ∑ i : Fin (d + 1), y i) : 1 ≤ (euclideanSimplexLinearForm y) (Grunbaum.simplexFullBody d).centroid

In dimension d + 1, the δ = 1 large-sum hypothesis in §2.2 puts the simplex centroid in the upper halfspace 1 ≤ L_y.

theorem Feige.grunbaumConstant_eq_sharpConstant (d : ℕ) : Grunbaum.grunbaumConstant d = sharpConstant (d + 1)