claimroutineinferred_dep

Wedge square identity bounds center discrepancy

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

Statement (paper)

For each

j\in[K]

\E_{(p,r)\sim\pi}\ip{U_j(p)}{U_j(r)}=\E_{q\sim\kappa}\left\|\E_{p\sim\omega(\cdot\mid q)}U_j(p)\right\|^2\ge0

. Consequently, by Cauchy--Schwarz first over

q

and then over the tests and step, the average absolute discrepancy is at most

B'\left(8B^2\sqrt{\frac{D}{2K}}\right)^{1/2}\le4BB'(D/K)^{1/4}

In plain English

For each step

j\in[K]

, the averaged inner product

\E_{(p,r)\sim\pi}\ip{U_j(p)}{U_j(r)}

equals

\E_{q\sim\kappa}\|\E_{p\sim\omega(\cdot\mid q)}U_j(p)\|^2

, which is nonnegative. Hence, by Cauchy–Schwarz over

q

and then over tests and step, the average absolute discrepancy is at most

B'(8B^2\sqrt{D/(2K)})^{1/2}\le 4BB'(D/K)^{1/4}

Why it's here

This turns the small averaged cross inner products from the previous claim into a bound on the discrepancy itself. Because

p

and

r

are conditionally independent given

q

under

\pi

, the cross term is a squared norm of a conditional mean, so it is a nonnegative quantity that dominates the square of the discrepancy after Cauchy–Schwarz. This gives the

(D/K)^{1/4}

rate in the parent lemma.

Classified routine:

Standard step: conditional independence of p and r given q turns the cross term into the squared norm of a conditional mean. Two Cauchy–Schwarz applications then convert the averaged inner-product bound from claim-pred-device-2 into the (D/K)^{1/4} discrepancy rate.

Uses

claimResidual inner products have small average

Used by

claimFresh test and fixed history

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Wedge square identity bounds center discrepancy" rests on claim-pred-device-2