claimroutineinferred_dep

Fresh test and fixed history

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

Statement (paper)

The average absolute discrepancy bound holds with the step test TJT_J replaced by a fresh test TT drawn independently after the strict prefix (J,T1,…,TJ−1)(J,T_1,\ldots,T_{J-1}), which is exactly . Consequently, averaging over strict prefixes, some fixed history HH, taking at most MK−1M^{K-1} possible values, has average absolute discrepancy over the fresh test at most 4BB′(D/K)1/44BB'(D/K)^{1/4}.

In plain English

The discrepancy bound 4BB′(D/K)1/44BB'(D/K)^{1/4} also holds when the step test TJT_J is replaced by a fresh test TT drawn independently after the prefix (J,T1,…,TJ−1)(J,T_1,\ldots,T_{J-1}). Hence some fixed history HH, among at most MK−1M^{K-1} possible values, has average absolute discrepancy over the fresh test at most this bound.

Why it's here

The previous claim bounds the discrepancy for the step test TJT_J. Since TJT_J is independent of the strict prefix and has the same law as a fresh TT, the two averages coincide, which gives . Averaging over prefixes then yields a single history that is at least as good as the average, and a history has at most MK−1M^{K-1} values because it consists of K−1K-1 codes in [M][M].
Classified routine:
Direct consequence of the previous claim: since T_J is independent of the strict prefix and has the same law as a fresh test, the two averages coincide. Choosing a history at least as good as the average is a standard averaging (pigeonhole) argument, and the count M^{K-1} comes from the history being K-1 codes in [M].

Uses

claimWedge square identity bounds center discrepancy

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Replace step test by fresh test; fix history" rests on claim-pred-device-3