lemmaroutine

Prefix history predicts test discrepancy

Lemma·pred:device·§3.1 The probability laws and the entropy comparison

Statement (paper)

Let ω,π,D\omega,\pi,D be as in --, let K,M≥1K,M\ge1 be integers, and let T1,…,TKT_1,\ldots,T_K be independent tests with the same law as TT. Each test specifies, in addition to cTc_T, a feature map fT:[M]→Rdf_T:[M]\to\R^d and a coefficient map gT:Q→Rdg_T:Q\to\R^d, for an integer d≥1d\ge1 and constants B,B′≥0B,B'\ge0, satisfying ∥fT(c)∥≤B,∥gT(q)∥≤B′ \norm{f_T(c)}\le B,\qquad \norm{g_T(q)}\le B' for all codes, centers and tests. Choose JJ uniformly from [K][K], independently of all tests, and retain only the strict prefix H(p)=(cT1(p),…,cTJ−1(p)). H(p)=(c_{T_1}(p),\ldots,c_{T_{J-1}}(p)). Conditioned on J,T1,…,TJ−1J,T_1,\ldots,T_{J-1}, let TT be a fresh test and define mT,h=∑x∈Pμh(x)fT(cT(x)). m_{T,h}=\sum_{x\in P}\mu_h(x)f_T(c_T(x)). Then EJ,T1,…,TJ−1,T∣E(p,q)∼ω⟨fT(cT(p))−mT,H(p),gT(q)⟩∣≤4BB′(DK)1/4. \E_{J,T_1,\ldots,T_{J-1},T} \left|\E_{(p,q)\sim\omega} \ip{f_T(c_T(p))-m_{T,H(p)}}{g_T(q)}\right| \le4BB'\left(\frac DK\right)^{1/4}. Every realized history has at most MK−1M^{K-1} values. In particular, a history can be fixed before drawing the fresh test so that its average absolute discrepancy in is at most the right side.

In plain English

Draw KK i.i.d. tests, pick a uniform step JJ, and keep only the codes of pp on the earlier tests as a history H(p)H(p). Then for a fresh test TT, the average of ∣E(p,q)∼ω⟨fT(cT(p))−mT,H(p),gT(q)⟩∣|\E_{(p,q)\sim\omega}\langle f_T(c_T(p))-m_{T,H(p)},g_T(q)\rangle| is at most 4BB′(D/K)1/44BB'(D/K)^{1/4}, and a single history with at most MK−1M^{K-1} possible values achieves this bound.

Why it's here

This is the main device of the section: a finite information budget DD means that, on average over steps, the history already predicts the next code well enough that the feature-minus-mean discrepancy is small. The proof sums conditional divergences to DD, uses Pinsker to bound the residual inner products, and uses the wedge square identity to turn those into a bound on the discrepancy. Replacing the step test by a fresh one and fixing a good history gives a bounded-size history, which the acceptance and cross corollaries use.
Classified routine:
This adapts the standard entropy-increment / pinning argument (as in Raghavendra–Tan correlation rounding or Montanari's pinning lemma). The chain rule spreads the information budget D over K steps, a uniformly random step has divergence at most D/K, and Pinsker plus Cauchy–Schwarz convert that into a small discrepancy.

Uses

Nothing else in the paper

Used by

corPrefix history predicts acceptance failurescorCross-pair error bound for true states

Inside the proof

claimConditional next-code divergences sum to DclaimResidual inner products have small averageclaimWedge square identity bounds center discrepancyclaimFresh test and fixed history

Sources

PaperOpen
Section
§3.1 The probability laws and the entropy comparison
Page
—
Label
pred:device
Line
sections/02-prediction.tex:78
Leannot aligned

Phase 2 aligns this node to a Lean declaration.