The proof in mathematics and Lean

From exchangeability to one hypergeometric count

Follow the reductions in ordinary mathematical language first, then inspect the exact Lean certificate attached to each step. The page keeps the paper's proof order visible from the initial symmetry reduction to the final consequences.

Formalization blueprint

The dependency graph at a glance

The graph follows the paper's proof direction from assumptions at the top to consequences at the bottom. Colors distinguish reduction, geometry, probability, and exported results.

ReductionGeometryProbabilityResult

Assumptions and normalization Exchangeability + centered padded weights IsExchangeableInLaw · centeredWeight

Section 3 · equation (1) Hamming-slice MGF inequality sliceMgf · centeredSphere

Geometry track

Lemma 2Hermite sign identitylemma_2_hermite_sign

Lemma 3Three-coordinate maximumlemma_3_three_coordinate

Proposition 2Two-level maximizerproposition_2_two_level

Probability track

Lemma 1Hoeffding's lemmalemma_1_hoeffding

Lemma 4Hypergeometric MGFlemma_4_hypergeometric

Constant track

Definition\(\gamma_{N,s}\) and \(\Gamma_N\)gammaTerm · Gamma

Finite maximumMaximum at \(\lfloor N/2\rfloor\)Gamma_eq_lastTerm

Theorem 1 Main exchangeable Hoeffding MGF bound theorem_1_mgf

Corollary 1Confidence boundcorollary_1

Lemma 5Barber comparisonlemma_5

Proposition 1Rate lower boundproposition_1

Remark 1Exact variational constantremark_1_variational

Numbering. The paper, this guide, and the Lean interface use the same labels: for example, Lemma 2 is lemma_2_hermite_sign and Theorem 1 is theorem_1_mgf.

How to read the detailed blocks

Mathematics first, formal certificate second

Paper target

The exact result or equation being proved.

Proof move

The mathematical reduction that advances the argument.

Lean certificate

The declaration that checks the claim.

Formal detail

An assumption or representation made explicit by Lean.

Paper · Theorem 1

\[ \log\mathbb E\left[\exp\left\{ \lambda\sum_{i=1}^n w_i(X_i-\bar X_N) \right\}\right] \le \frac{\lambda^2}{2}\Gamma_N \lVert P_{\mathbf1^\perp}\widetilde w\rVert_2^2. \]

Lean · theorem statement

theorem theorem_1_mgf
    {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] {N n : ℕ}
    (hN : 2 ≤ N) (hn : n ≤ N) (X : Ω → Fin N → ℝ)
    (hXmeas : ∀ j, StronglyMeasurable (fun ω ↦ X ω j))
    (hX : ∀ ω j, (-1 : ℝ) ≤ X ω j ∧ X ω j ≤ 1)
    (hEx : IsExchangeableInLaw μ X)
    (w : Fin n → ℝ) (lam : ℝ) :
    Real.log (exchangeableMgf μ hn X w lam) ≤
      lam ^ 2 / 2 * Gamma N * sqNorm (centeredWeight hn w)

Reduction to Hamming slices

Remove the order and reduce the cube to a subset

Set \(a=P_{\mathbf1^\perp}\widetilde w\). Because \(\sum_i a_i=0\), the centered statistic equals \(a^\top X\). Exchangeability allows an average over all coordinate permutations; convexity then moves the maximum from \([-1,1]^N\) to a sign vector.

If exactly \(k\) coordinates of the sign vector are positive, their permuted locations form a uniform \(k\)-subset \(S_k\). Substituting \(y_i=2\lambda a_i\) reduces Theorem 1 to the paper's equation (1):

Paper · equation (1)

\[ \log\mathbb E_{S_k}\left[\exp\left\{\sum_{i\in S_k}y_i\right\}\right] \le \frac{\Gamma_N}{8}\lVert y\rVert_2^2, \qquad \sum_{i=1}^N y_i=0. \tag{1} \]

Lean · paper-facing interfaces

lemma_1_hoeffding
lemma_2_hermite_sign
lemma_3_three_coordinate
proposition_2_two_level
lemma_4_hypergeometric
theorem_1_mgf

Paper target

Equation (1), uniformly in the slice size \(k\).

Proof move

Center weights → average permutations → use convexity → condition on the number of \(+1\) coordinates.

Lean certificate

centeredWeight, IsExchangeableInLaw, sliceMgf, and centeredSphere.

Formal detail

The probability law, coordinate measurability, boundedness, and zero-sum identity are represented explicitly.

Proposition 2

A slice maximizer has at most two coordinate values

Fix \(\sum_i y_i=0\) and \(\lVert y\rVert_2=\rho\). If a maximizer had three distinct coordinates, the Lagrange multiplier conditions on that three-coordinate sphere section would contradict the positive Hermite derivative identity of Lemma 2. Lemma 3 packages that local contradiction; Proposition 2 applies it to every triple.

Lemma 2lemma_2_hermite_sign→Lemma 3lemma_3_three_coordinate→Proposition 2proposition_2_two_level

If \(\alpha\) occurs \(m\) times and \(\beta\) occurs \(N-m\) times, with \(d=\alpha-\beta\), the constraints determine the two levels exactly:

Paper · equation (2)

\[ \alpha=\frac{N-m}{N}d, \qquad \beta=-\frac{m}{N}d, \qquad d^2=\rho^2\frac{N}{m(N-m)}. \tag{2} \]

Lean · Proposition 2

theorem proposition_2_two_level
    {N K : ℕ} (hN : 2 ≤ N)
    (hK0 : 1 ≤ K) (hKN : K ≤ N - 1)
    {rhoSq : ℝ} (hrho : 0 ≤ rhoSq) {y : Fin N → ℝ}
    (hy : y ∈ centeredSphere N rhoSq) :
    ∃ z ∈ centeredSphere N rhoSq,
      (∀ x ∈ centeredSphere N rhoSq,
        sliceMgf N K x ≤ sliceMgf N K z) ∧
      HasAtMostTwoValues z

Paper target

Proposition 2: existence of a two-level maximizer for the slice objective.

Proof move

Hermite interpolation sign → second-order obstruction → repeated coordinate → global two-level structure.

Lean certificate

lemma_2_hermite_sign → lemma_3_three_coordinate → proposition_2_two_level.

Formal detail

Compactness, existence of a maximizer, the degenerate radius, and the admissible elementary-symmetric terms are handled separately.

Lemma 4 and the constant

The two-level sum is hypergeometric

Let \(A\) be the \(m\)-coordinate level set. For a uniform \(k\)-subset,

\[ H=|S_k\cap A|\sim\operatorname{Hypergeometric}(N,k,m), \qquad \mathbb EH=\frac{km}{N}. \]

The subset sum is \(d(H-km/N)\). With \(s=m\wedge(N-m)\), Lemma 4 proves

Paper · Lemma 4

\[ \log\mathbb E\left[e^{t(H-km/N)}\right] \le\frac{t^2}{8}B_{N,m}, \qquad B_{N,m}=(N-s)^2\sum_{\ell=N-s}^{N-1}\frac1{\ell^2}. \]

Lean · Lemma 4

theorem lemma_4_hypergeometric
    {N K m : ℕ} (hN : 2 ≤ N) (hK : K ≤ N)
    (hm0 : 1 ≤ m) (hmN : m ≤ N - 1) (t : ℝ) :
    Real.log (mgf N K m t) ≤
      t ^ 2 / 8 * martingaleFactor N m := by
  have huniv := log_mgf_le_universal hN hK
    (by omega : m ≤ N) t
  have hfactor := sampleVarianceFactor_le_martingaleFactor
    hN hm0 hmN
  -- algebra converts the stronger coefficient to B_{N,m}

Combining this with equation (2) produces

\[ \gamma_{N,s}= \frac{N(N-s)}s\sum_{\ell=N-s}^{N-1}\frac1{\ell^2} \le \Gamma_N, \]

which closes equation (1), and hence Theorem 1.

Paper target

Lemma 4 followed by the last inequality in the proof of Theorem 1.

Proof move

Sampling-without-replacement martingale → conditional Hoeffding lemma → complement symmetry → maximize \(\gamma_{N,s}\).

Lean certificate

lemma_1_hoeffding, lemma_4_hypergeometric, gammaTerm, and Gamma.

Formal detail

The Lean hypergeometric interface is derived from a stronger finite-population coefficient, then weakened to the paper's \(B_{N,m}\).

Constant arithmetic

Closed form, asymptotics, and comparison

A half-integer telescoping estimate proves that \(\gamma_{N,s}\) is nondecreasing for \(1\le s\le\lfloor N/2\rfloor\). Thus \(\Gamma_N\) is the last term:

\[ \Gamma_N= \begin{cases} N\displaystyle\sum_{\ell=N/2}^{N-1}\ell^{-2}, & N\text{ even},\\[1em] \dfrac{N(N+1)}{N-1}\displaystyle\sum_{\ell=(N+1)/2}^{N-1}\ell^{-2}, & N\text{ odd}. \end{cases} \]

Lean certificate chain

inverseSquareTail_upper_half

Half-integer telescoping estimate.

gammaTerm_mono_step → gammaTerm_mono

Stepwise and interval monotonicity.

Gamma_eq_lastTerm

The finite maximum occurs at \(s=\lfloor N/2\rfloor\).

Gamma_closedForm_even, Gamma_closedForm_odd

The two parity formulas in Theorem 1.

Gamma_asymptotic

The expansion \(\Gamma_N=1+3/(2N)+O(N^{-2})\).

lemma_5, lemma_5_eq_two

Lemma 5: strict comparison for \(N\ge3\), equality at \(N=2\).

Consequences and sharpness

What follows from the main theorem

Corollary 1

Confidence bound

Chernoff optimization gives the threshold \(\lVert P_{\mathbf1^\perp}\widetilde w\rVert_2\sqrt{2\Gamma_N\log(1/\delta)}\).

corollary_1

Lemma 5

Comparison with Barber

\(\Gamma_N<1+\epsilon_N\) for \(N\ge3\), with equality at \(N=2\).

lemma_5

Proposition 1

Rate lower bound

Every uniform coefficient is at least \(N/(N-1)\) for even \(N\) and \((N+1)/N\) for odd \(N\).

proposition_1

Remark 1

Exact variational constant

The hypergeometric variational supremum equals the exact optimal exchangeable coefficient.

remark_1_variational

Open the complete declaration map →