EHFormalization guide

Paper-to-Lean cross-reference

Declaration map

Search by result number, mathematical role, or Lean declaration. Each entry connects a statement in the paper to its checked formal counterpart.

14 result groups

Numbering. The paper labels and Lean declaration numbers agree: Theorem 1 is theorem_1_mgf, Lemma 4 is lemma_4_hypergeometric, and so on.

Theorem 1

Main MGF inequality

Logarithmic form of the paper's exponential moment bound.

Tail form and Corollary 1

One-sided concentration

Arbitrary-threshold Chernoff form and confidence-parameter specialization.

Inflation factor

Literal finite maximum

Encodes \(\gamma_{N,s}\) and \(\Gamma_N=\max_s\gamma_{N,s}\).

Maximizing index

Monotonicity

Shows that the maximum occurs at \(s=\lfloor N/2\rfloor\).

Parity formulas

Closed forms

The even and odd displays appearing with Theorem 1.

Asymptotics

Second-order expansion

\(\Gamma_N=1+3/(2N)+O(N^{-2})\), obtained from quantitative parity bounds.

Lemma 1

Hoeffding's lemma

Measure-theoretic MGF bound for a centered bounded random variable.

Lemma 2

Hermite sign identity

Positive weighted derivative sum at three ordered roots.

Lemma 3

Three-coordinate section

A constrained global maximizer has a repeated coordinate.

Proposition 2

Two-level maximizer

The slice MGF has a maximizer with at most two coordinate values.

Lemma 4

Hypergeometric MGF

The centered log-MGF bound with the paper's coefficient \(B_{N,m}\).

Lemma 5

Comparison with Barber

Strict improvement for \(N\ge3\) and equality at \(N=2\).

Proposition 1

Rate lower bound

Parity-dependent lower bound for every uniform exchangeable coefficient.

Remark 1

Exact variational constant

Identifies the literal hypergeometric supremum with the exact optimal coefficient.

Notation dictionary

Translate the paper into Lean

\(\widetilde w\)zeroPad hn w

Extend \(n\) weights to \(N\) coordinates.

\(P_{\mathbf1^\perp}\widetilde w\)centeredWeight hn w

Remove the constant component.

\(\lVert P_{\mathbf1^\perp}\widetilde w\rVert_2^2\)sqNorm (centeredWeight hn w)

Squared projected norm.

ExchangeabilityIsExchangeableInLaw μ X

Permutation-invariance of the pushforward law.

Subset exponential averagesliceMgf N K y

Uniform average over fixed-size subsets.

\(B_{N,m}\)martingaleFactor N m

Hypergeometric MGF coefficient.

\(\Gamma_N\)Gamma N

Explicit inflation factor.

\(\mathcal V_N\)variationalConstant N

Exact hypergeometric variational supremum.

Verification

Reproduce the checks

Show commands
Project root
lake build
lake env lean AxiomAudit.lean
rg -n '\b(sorry|admit)\b|^\s*axiom\b|\b(unsafe|implemented_by)\b' . --glob '*.lean' --glob '!**/.lake/**'

The axiom audit is expected to report only the standard logical foundations inherited from Lean/mathlib: propext, Classical.choice, and Quot.sound.

Copied