← All papers
First page of Stochastic Domination of Gaussian Maxima by the Regular Simplex

Stochastic Domination of Gaussian Maxima by the Regular Simplex

Abhijeet Mulgund

math.PR Sep 23, 2026 · v2 cs.IT math.MG
A Lean formalization accompanies the proof that the regular simplex minimizes Gaussian measure among simplices containing a given ball.
Let $n\ge2$, and let $X=(X_1,\ldots,X_n)$ be a centered Gaussian vector with $\mathrm{Var}(X_i)=1$ for every $i$. Let $Z_1,\ldots,Z_n$ be independent standard Gaussians, and put $\overline{Z}=(Z_1+\cdots+Z_n)/n$. We prove $\mathbb{P}\{\max_i X_i\le t\}\ge\mathbb{P}\{\sqrt{n/(n-1)}\,\max_i(Z_i-\overline{Z})\le t\}$ for every $t\in\mathbb{R}$, and for each fixed $t>0$ equality holds only when $\mathrm{Cov}(X_i,X_j)=-1/(n-1)$ for all $i\ne j$. The right side is the distribution function of the maximum of the regular simplex vector. Equivalently, among all simplices containing a given centered ball, the regular simplex circumscribed about the ball has the least standard Gaussian measure, as conjectured by Balitskiy, Karasev, and Tsigler. In our preceding paper we proved this comparison after both maxima are smoothed by independent Gaussian noise of variance $1/(n-1)$, which suffices for the Weak Simplex Conjecture; here we remove the smoothing, which is what probabilities at a single threshold require. As an application we consider $n$ equally likely signals of equal energy in Gaussian noise, where the transmitter may also send nothing. At every positive false-alarm level, and for every law of a common nonnegative random amplitude not concentrated at zero, the regular simplex uniquely maximizes the average probability of correct identification whenever the signal dimension is at least $n-1$. A Lean formalization is available at https://github.com/abhmul/full-simplex-conjecture-lean.

Balitskiy, Karasev, and Tsigler conjectured that among all simplices in R^{n-1} containing a centered ball, the regular simplex circumscribed about the ball has least Gaussian measure. Equivalently, the regular simplex vector stochastically dominates the maximum of any centered unit-variance Gaussian vector at every threshold.

The comparison P{max X_i <= t} >= P{max ξ_i <= t} is reduced to a derivative bound at a minimizing covariance over the compact set of correlation matrices. First-order conditions from adding independent Gaussian noise yield structural constraints on minimizers, and an aggregate bound using log-concavity and a dilation identity establishes the inequality with its equality case. A Lean formalization of the argument is provided.

The full simplex conjecture is proved in every dimension, with equality only for the regular simplex correlation -1/(n-1). Applications include that the regular simplex uniquely maximizes correct-identification probability with an inactive state at every positive false-alarm level.