claimroutineinferred_dep

Interpolation interval captures binomial mass

Claim·§4.7 Choosing the parameters·inside lemExplicit parameter choice satisfies layout hypotheses

Statement (paper)

Let μ=Q(r−1)2r\mu=\frac{Q(r-1)}{2r}, A0=⌊μ−R−12⌋A_0=\lfloor\mu-\frac{R-1}{2}\rfloor and I={A0,…,A0+R−1}\mathcal I=\{A_0,\ldots,A_0+R-1\}. Then, for sufficiently large nn, I⊆{0,…,Q}\mathcal I\subseteq\{0,\ldots,Q\}, and for W∼Bin⁡(Q,(r−1)/(2r))W\sim\operatorname{Bin}(Q,(r-1)/(2r)) one has Pr⁡[W∉I]⩽2e−R2/(8Q)⩽1br2λ=ϵ\Pr[W\notin\mathcal I]\le 2e^{-R^2/(8Q)}\le\frac1{br^2\lambda}=\epsilon, which is with ϵ=τ/(rb)\epsilon=\tau/(rb). Moreover 0<τ⩽1/20<\tau\le1/2.

In plain English

With μ=Q(r−1)2r\mu=\frac{Q(r-1)}{2r}, the interval I\mathcal I of RR consecutive integers starting at A0=⌊μ−R−12⌋A_0=\lfloor\mu-\frac{R-1}{2}\rfloor lies inside {0,…,Q}\{0,\ldots,Q\} for large nn. A variable W∼Bin⁡(Q,(r−1)/(2r))W\sim\operatorname{Bin}(Q,(r-1)/(2r)) falls outside I\mathcal I with probability at most 2e−R2/(8Q)⩽ϵ=1br2λ2e^{-R^2/(8Q)}\le\epsilon=\frac1{br^2\lambda}, and 0<τ⩽1/20<\tau\le1/2.

Why it's here

This gives the tail bound that the layout lemma needs, with ϵ=τ/(rb)\epsilon=\tau/(rb). The interval is centred at the binomial mean μ\mu and has width R=Θβ(λ)R=\Theta_\beta(\sqrt\lambda), so a Hoeffding-type bound gives a tail of e−Ω(R2/Q)e^{-\Omega(R^2/Q)}. Taking the constant β+3\beta+3 in RR makes this tail at most 1/(br2λ)1/(br^2\lambda), using the size bounds on rr, QQ, RR from the previous claim.
Classified routine:
Direct application of Hoeffding's inequality (Hoeffding 1963) to a binomial variable centred at its mean, combined with the parameter size bounds from the previous claim; pure parameter bookkeeping.

Sources

PaperOpen
Section
§4.7 Choosing the parameters
Page
—
Label
—
Line
main_full_version.tex:2796
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Interpolation interval and binomial tail bound" rests on claim-lem-incidence-parameters-1