claimroutineinferred_dep

Residual inner products have small average

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

Statement (paper)

For the fixed test sequence, with

U_j(p)=f_{T_j}(c_{T_j}(p))-\sum_x\mu_{H_j(p)}(x)f_{T_j}(c_{T_j}(x))

, one has

\norm{U_j(p)}\le 2B

and

\frac1K\sum_{j=1}^K\E_{(p,r)\sim\pi}\ip{U_j(p)}{U_j(r)}\le 8B^2\sqrt{\frac{D}{2K}}

In plain English

For a fixed test sequence, the residual vectors

U_j(p)

, the feature of

p

's code minus the mean feature under the history-conditioned law, have norm at most

2B

. Their averaged cross inner products over

(p,r)\sim\pi

satisfy

\frac1K\sum_{j}\E\ip{U_j(p)}{U_j(r)}\le 8B^2\sqrt{D/(2K)}

Why it's here

The norm bound follows from

\norm{f_T}\le B

and the mean being an average of such vectors. The inner-product bound turns the total divergence budget

D

from the previous claim into a per-step smallness: by Pinsker, each step's total-variation distance is at most

\sqrt{\text{KL}/2}

, and Cauchy–Schwarz over

j

gives the

\sqrt{D/(2K)}

average. This feeds the wedge square identity, which gives the

(D/K)^{1/4}

bound in the parent lemma.

Classified routine:

Follows from the previous divergence-sum claim by Pinsker's inequality and Cauchy–Schwarz over the steps. This is a standard bookkeeping step, like those in entropy-increment / 'pinning' arguments.

Uses

claimConditional next-code divergences sum to D

Used by

claimWedge square identity bounds center discrepancy

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Residual inner products have small average" rests on claim-pred-device-1