From simplex geometry to the exponential statistic

The paper defines Kₙ by normalized simplex volume in (2.1). The formalization also uses an equivalent independent-exponential representation. This file records their identification and proves that the α = 0 centroid-halfspace theorem supplies the δ = 1 LargeSumBridge consumed by the final reduction.

def Feige.SimplexExponentialIdentification (n : ℕ) : Prop

Equality of the simplex-volume and exponential presentations of the Dirichlet statistic.

Equations

• Feige.SimplexExponentialIdentification n = ∀ (y : Fin n → ℝ), Feige.dirichletK y = Feige.simplexK y

theorem Feige.dirichletK_largeSumBridge_of_simplex {n : ℕ} (hid : SimplexExponentialIdentification n) (hcentroid : SimplexCentroidHalfspaceProperty) : LargeSumBridge dirichletK

The δ = 1 geometric estimate in §2.2 for dirichletK, reduced to the distributional identification and the simplex centroid-halfspace bound.