Exchangeable Hoeffding — Formalization Guide

1 · The problem

Compare measurements with their shared average

We observe \(N\) measurements \(X_1,\ldots,X_N\), each between \(-1\) and \(1\). They are exchangeable: rearranging their labels leaves their joint probability law unchanged. They can still be dependent.

For example, shuffle three \(+1\)'s and one \(-1\), and reveal them in order. Each position has the same distribution. Once you see the first three values, however, the fourth is determined.

Choose weights \(w_1,\ldots,w_n\) for \(n\le N\) positions. The quantity we want to control is their weighted deviation from the full average:

\[ \begin{gathered} T=\sum_{i=1}^{n}w_i(X_i-\bar X_N),\\[.5em] \bar X_N=\frac1N\sum_{i=1}^N X_i. \end{gathered} \]

Try it with four measurements

Choose a comparison, then rearrange the values. Their full average stays at \(1/2\).

Comparison

Four coordinates: measurements and their coefficients
Position	1	2	3	4
Values	+1	+1	+1	−1
Weights	1/2	1/2	0	0
Centered weights	1/4	1/4	−1/4	−1/4

The first two average to 1, so T = 1 − 1/2 = 1/2.

Why center the weights?

Add zero weights for unused positions, then subtract the average of those \(N\) weights. The new coefficients sum to zero and give exactly the same statistic: \(T=\sum_{i=1}^N a_iX_i\).

In the initial example, subtract \(1/4\) from each weight. This changes \((1/2,1/2,0,0)\) into \((1/4,1/4,-1/4,-1/4)\). These are the coefficients that enter the bound.

The paper writes this centered vector as \(a=P_{\mathbf1^\perp}\widetilde w\). Here \(\widetilde w\) means the weights after adding zeros; \(P_{\mathbf1^\perp}\) removes their constant component.

2 · The bound

The size of the centered weights controls the fluctuations

Let \(a_i\) denote the centered weights, shown in the last row of the table. For \(N\ge2\), write \(A=\sum_{i=1}^N a_i^2\) for their squared size. Theorem 1 bounds the moment generating function, the average of the exponential \(e^{\lambda T}\):

\[ \mathbb E[e^{\lambda T}]\le e^{\lambda^2\Gamma_N A/2}. \]

\(T\): The weighted comparison from the example above.
\(A\): The sum of squared centered weights. In the initial example, \(A=4(1/4)^2=1/4\).
\(\Gamma_N\): An explicit factor depending only on the number of measurements. It approaches 1 as \(N\) grows.
\(\lambda\): A real tuning parameter. The inequality holds for every choice of it.

How does this bound a large deviation?

For \(A>0\) and a threshold \(t>0\), applying Markov's inequality to \(e^{\lambda T}\) and optimizing over \(\lambda>0\) gives:

\[ \mathbb P(T\ge t)\le \exp\!\left(-\frac{t^2}{2\Gamma_N A}\right). \]

For fixed \(t\), a smaller \(A\) or \(\Gamma_N\) gives a smaller upper bound. If \(A=0\), all centered weights are zero and \(T=0\) identically.

Read Theorem 1 in the paper's notation

Assume \(N\ge2\), \(n\le N\), and exchangeable \(X_i\in[-1,1]\). The weights are arbitrary real numbers, including negative ones. For every \(\lambda\in\mathbb R\):

\[ \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\}. \]

The shorter display above uses \(T\) for the sum on the left and \(A=\lVert P_{\mathbf1^\perp}\widetilde w\rVert_2^2\) for the squared norm on the right.

Find the corresponding Lean declarations

Lean is a proof assistant. These declarations connect the mathematical statements to their formal proofs.

Centered weights: centeredWeight hn w
Squared size \(A\): sqNorm (centeredWeight hn w)

Open the complete Lean reference →

3 · The proof idea

Turn a weighted sum into a count

The proof reduces a problem about many real coefficients to one about sampling a subset. Each step removes a different source of complexity.

Use symmetry to forget the order
Exchangeability permits averaging over all rearrangements. Convexity reduces the bounded values to \(+1\) and \(-1\). With \(k\) positive signs, their locations form a uniformly chosen \(k\)-element subset.
The term “Hamming slice”
All sign vectors with exactly \(k\) positive entries form a Hamming slice. Choosing a vector on that slice is equivalent to choosing the subset of its positive positions.
Choose a worst-case vector with just two values
Among centered coefficient vectors of a fixed squared size, Proposition 2 lets us choose a maximizer with at most two levels: an upper value \(\alpha\) and a lower value \(\beta\).
Why are two levels enough?
Lemma 2 and Lemma 3 give a local obstruction to three distinct coordinate values at a maximizer. Proposition 2 applies this to every triple. The proof guide gives the full argument.
Count how many selected entries are at the upper level
Once there are just two values, the subset sum depends only on this count \(H\). Under uniform sampling without replacement, \(H\) has a hypergeometric distribution. Lemma 4 bounds its exponential moment.

See the last step with eight coefficients3 upper values · 5 lower values · choose 4

Each vertical line is one coefficient. Rings in the bottom row mark the four selected positions; filled centers mark selected upper values.

Positions 1, 3, 5, 8: 2 upper values and 2 lower values. The sum is 2 × (5/8) + 2 × (−3/8) = 1/2.

What to notice. The upper value is \(\alpha=5/8\); the lower value is \(\beta=-3/8\). Changing the selected positions changes the count \(H\). Subsets with the same \(H\) have the same sum.

Connect the picture to the general formula

There are \(N\) coordinates, of which \(m\) have the upper value. We select \(k\) of them without replacement. The expected number of upper values is \(km/N\).

\[ \sum_{i\in S}y_i=(\alpha-\beta)\left(H-\frac{km}{N}\right). \]

Here \(N=8\), \(m=3\), \(k=4\), and \(\alpha-\beta=1\), so the sum is \(H-3/2\). This example illustrates the reduction; the proof establishes it for the general two-level vector.

Continue to the detailed proof →

What does the factor \(\Gamma_N\) look like?

The factor approaches 1 as the number of measurements grows. For large \(N\), a useful approximation is:

\[ \Gamma_N\approx1+\frac{3}{2N}. \]

The main correction above 1 is proportional to \(1/N\). The exact formula and the formal asymptotic expansion are below.

See the exact definition

\[ \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}. \]

The maximum occurs at \(s=\lfloor N/2\rfloor\). Its formalized expansion is \(\Gamma_N=1+3/(2N)+O(N^{-2})\): the remainder is of order \(1/N^2\).

Lemma 5 also compares it with the earlier coefficient \(1+\epsilon_N\): \(\Gamma_N<1+\epsilon_N\) for \(N\ge3\).

The proof guide records the even and odd closed forms and their Lean certificates.

Technical notes on the formalization

The weak-tail corollary at zero norm

The checked Corollary 1 assumes \(A>0\). At zero projected norm, its weak event becomes \(\{0\ge0\}\), whose probability is one. A strict-tail formulation handles the degenerate case automatically.

Optimality is a separate claim

Proposition 1 gives the parity-dependent rate lower bound. Remark 1 identifies the exact variational coefficient. The declaration map records both separately from the MGF upper bound.

Where to go next

Follow the mathematical proof →Each reduction, the supporting lemmas, and optional Lean statements. Look up a Lean declaration →Search by theorem number, notation, or declaration name. Read the paper →The full statements, context, and original argument.

A sharper Hoeffding bound for weighted sums of exchangeable random variables