Asymptotic size
\(\displaystyle \Gamma_N=1+\frac{3}{2N}+O(N^{-2})\)
Exchangeability, concentration, and formal verification
A sharper Hoeffding bound for weighted sums of exchangeable random variables
This guide explains how exchangeability turns an arbitrary signed weighted sum into a finite subset problem, why a two-level extremizer is enough, and where Lean checks each step.
Theorem 1
The main MGF inequality
Let \(X_1,\ldots,X_N\in[-1,1]\) be exchangeable and let \(w_1,\ldots,w_n\) be arbitrary real weights. Extend the weights by zero to \(\widetilde w\in\mathbb R^N\), then project away their constant component. This leaves exactly the part of the weights that can contribute to a centered contrast.
\[
\mathbb E\left[\exp\left\{
\lambda\sum_{i=1}^n w_i(X_i-\bar X_N)
\right\}\right]
\le
\exp\left\{
\frac{\lambda^2}{2}\Gamma_N
\lVert P_{\mathbf1^\perp}\widetilde w\rVert_2^2
\right\}.
\]
Paper\(P_{\mathbf1^\perp}\widetilde w\)→
centeredWeight hn wPaper\(\lVert P_{\mathbf1^\perp}\widetilde w\rVert_2^2\)→
sqNorm (centeredWeight hn w)Lean certificate
How to read the formula. The squared centered-weight norm measures the size of the contrast, while \(\Gamma_N\) is the exchangeability inflation factor. The paper's Theorem 1 is checked by theorem_1_mgf.
The paper's three proof steps
How arbitrary weights become one count
This is the proof order stated at the beginning of Section 3. The blueprint page expands every arrow into its mathematical move and Lean certificate.
-
1
Reduce to the Hamming-slice inequality (1)
Center the weights, average over permutations, use convexity, and condition on the number of positive signs.
-
2
Reduce a slice maximizer to two levels
Lemma 2 and Lemma 3 supply the local geometry; Proposition 2 converts the high-dimensional maximizer into two coordinate values.
-
3
Apply the hypergeometric MGF bound
The two-level subset sum is a centered hypergeometric random variable. Lemma 4 and the definition of \(\Gamma_N\) close inequality (1).
The constant
An explicit improvement
The inflation factor is not left implicit: it is an explicit finite maximum whose maximizing index, parity-dependent closed forms, and asymptotic expansion are all formalized.
\[
\Gamma_N=
\max_{1\le s\le\lfloor N/2\rfloor}
\frac{N(N-s)}s
\sum_{\ell=N-s}^{N-1}\frac1{\ell^2}.
\]
Lemma 5
\(\displaystyle \Gamma_N<1+\epsilon_N\quad(N\ge3)\)
Formalization clarity
What the guide makes explicit
The paper's proof order
The guide follows the mathematical argument in its original order: symmetry, a Hamming slice, a two-level extremizer, a centered hypergeometric MGF, and finally Theorem 1.
The weak-tail corollary at zero norm
The checked Corollary 1 assumes \(P_{\mathbf1^\perp}\widetilde w\ne0\). At zero projected norm, the displayed weak event becomes \(\{0\ge0\}\), whose probability is one. A strict-tail formulation would make the degenerate case automatic.
Optimality is a separate claim
Proposition 1 gives the parity-dependent rate lower bound, while Remark 1 identifies the exact variational coefficient. The declaration map records both statements separately from the MGF upper bound.