claimroutineinferred_dep

Averaging over binomial clean count

Averaging over the clean count gives (1−β2−dim⁡W−rs/3600)k(1-\beta 2^{-\dim W-r_{\rm s}}/3600)^k
turns conditional decay into the lemma's bound
Claim·§6.2 Vanishing advice on clean coordinates·inside lemAdvice agreement decays with clean coordinates

Statement (paper)

Conditional on AA, the size ∣I∣|I| of the clean set has distribution Binomial⁡(k,pA)\operatorname{Binomial}(k,p_A), and averaging the conditional bound Pr⁡[πˉaU=aO∣R=r]≤(1−1/3600)∣I∣\Pr[\bar\pi a_U=a_O\mid R=r]\le(1-1/3600)^{|I|} first over RR given AA and then over AA gives Pr⁡[πˉ(aU)=aO]≤EA(1−pA3600)k≤(1−β 2−dim⁡W−rs3600)k≤exp⁡ ⁣(−kβ 2−dim⁡W−rs3600)\Pr\bigl[\bar\pi(a_U)=a_O\bigr]\le \E_A\left(1-\frac{p_A}{3600}\right)^k\le\left(1-\frac{\beta\,2^{-\dim W-r_{\rm s}}}{3600}\right)^k\le\exp\!\left(-\frac{k\beta\,2^{-\dim W-r_{\rm s}}}{3600}\right), using rank⁡A≤rs\rank A\le r_{\rm s}; with kβ=k1/3k\beta=k^{1/3} this yields Equation .

In plain English

Averaging the conditional agreement bound over the random clean set II and over the advice AA gives Pr⁡[πˉ(aU)=aO]≤(1−β2−dim⁡W−rs/3600)k≤exp⁡(−kβ2−dim⁡W−rs/3600)\Pr[\bar\pi(a_U)=a_O]\le(1-\beta 2^{-\dim W-r_{\rm s}}/3600)^k\le\exp(-k\beta 2^{-\dim W-r_{\rm s}}/3600), which with kβ=k1/3k\beta=k^{1/3} is the bound of the lemma.

Why it's here

Given AA, the clean count ∣I∣|I| is Binomial⁡(k,pA)\operatorname{Binomial}(k,p_A) by the previous clean-coordinate claim, so E(1−1/3600)∣I∣=(1−pA/3600)k\E(1-1/3600)^{|I|}=(1-p_A/3600)^k. Since rank⁡A≤rs\rank A\le r_{\rm s} gives pA≥β2−dim⁡W−rsp_A\ge\beta 2^{-\dim W-r_{\rm s}}, the bound becomes uniform in AA, and this turns the repeated-game decay of the conditional bound into the stated decay in kk.
Classified routine:
A direct calculation from the earlier claims: the binomial moment-generating identity E[(1-c)^{Bin(k,p)}]=(1-cp)^k, a uniform lower bound on p_A from the rank bound, and the inequality 1-x <= e^{-x}.

Uses

claimConditional agreement bounded by repeated gameclaimClean coordinates have ordinary question law

Used by

Nothing in the paper

Sources

PaperOpen
Section
§6.2 Vanishing advice on clean coordinates
Page
—
Label
—
Line
sections/05-clean.tex:223
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Averaging over binomial clean count" rests on claim-lem-clean-5
  • info
    inferred_dep
    outline: "Averaging over binomial clean count" rests on claim-lem-clean-2