corollaryroutineinferred_dep

Prefix history predicts acceptance failures

Corollary·pred:acceptance·§3.2 Acceptance tests and the prediction coupling

Statement (paper)

In the setting of , suppose each test specifies a set

\mathcal A_T(q)\subseteq[M]

of accepted codes for every

q\in Q

. Put

s_0=\E_T\Prob_{(p,q)\sim\omega} \{c_T(p)\notin\mathcal A_T(q)\}.

There is a fixed strict-prefix history

H

, with at most

M^{K-1}

values, such that

\E_T\sum_{p,q}\omega(p,q) \sum_x\mu_{H(p)}(x) \mathbf1_{\{c_T(x)\notin\mathcal A_T(q)\}} \le s_0+4\sqrt M(D/K)^{1/4}.

The fresh test

T

is independent of the fixed history construction.

In plain English

If each test

T

accepts a set

\mathcal A_T(q)

of codes for each

q

, and

s_0

is the average rate at which

c_T(p)

is rejected under

\omega

, then a single history

H

with at most

M^{K-1}

values exists. Sampling

x

from the predicted distribution

\mu_{H(p)}

instead of using the true code gives an average rejection rate of at most

s_0+4\sqrt M(D/K)^{1/4}

Why it's here

This turns the discrepancy bound of the prefix-history lemma into a statement about acceptance tests: a rejection indicator is a bounded inner-product test, so the history-based prediction fails at most slightly more often than the true code does. Later results use it to replace the true code by a predicted one from a bounded history while keeping the rejection rate under control, as in the quantization-test step and the bounded-alternative argument.

Classified routine:

Direct consequence of the prefix-history discrepancy lemma (pred-device), applied with the bounded test function given by the rejection indicator. Comparing against s_0 is bookkeeping plus the fact that some fixed history attains the expectation over the random history.

Uses

lemPrefix history predicts test discrepancy

Used by

propTotal variation S cannot stay boundedclaimQuantized acceptance tests with a history predictor

Sources

PaperOpen

Section: §3.2 Acceptance tests and the prediction coupling
Page: —
Label: pred:acceptance
Line: sections/02-prediction.tex:185

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: Corollary pred:acceptance is stated "In the setting of " (02-prediction.tex:186) and its proof averages (line 208).