claimroutine

Conditional next-code divergences sum to D

Claim·§3.1 The probability laws and the entropy comparison·inside lemPrefix history predicts test discrepancy

Statement (paper)

For a fixed sequence of tests T1,…,TKT_1,\ldots,T_K, with HjH_j the transcript strictly before step jj, aj,h,h′a_{j,h,h'} the actual conditional law of the next two codes and bj,h,h′=(cTj)∗μh⊗(cTj)∗μh′b_{j,h,h'}=(c_{T_j})_*\mu_h\otimes(c_{T_j})_*\mu_{h'} the reference next-code law, one has ∑j=1KE(p,r)∼πDKL⁡(aj,Hj(p),Hj(r)∥bj,Hj(p),Hj(r))≤D. \sum_{j=1}^K \E_{(p,r)\sim\pi}\KL\bigl(a_{j,H_j(p),H_j(r)}\Vert b_{j,H_j(p),H_j(r)}\bigr)\le D.

In plain English

For a fixed sequence of tests T1,…,TKT_1,\ldots,T_K, the total over steps jj of the expected KL divergence (over (p,r)∼π(p,r)\sim\pi) between the actual conditional law of the next two codes and the reference product law (cTj)∗μh⊗(cTj)∗μh′(c_{T_j})_*\mu_h\otimes(c_{T_j})_*\mu_{h'}, given the histories Hj(p),Hj(r)H_j(p),H_j(r), is at most DD.

Why it's here

This is a chain-rule step: the per-step conditional divergences add up to a total information budget bounded by DD, so on average over jj they are small (at most D/KD/K). The next claim uses this to show that the residual inner products Uj(p)U_j(p) have small average, which then yields the (D/K)1/4(D/K)^{1/4} bound in the parent lemma.
Classified routine:
Direct application of the chain rule for KL divergence, together with the data-processing inequality, to the joint law of the code transcript against a product reference law whose total divergence is D.

Uses

Nothing else in the paper

Used by

claimResidual inner products have small average

Sources

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

Phase 2 aligns this node to a Lean declaration.