claimroutineinferred_dep

Averaging bounds distinct-pair budget by 10δ²λC_i

Claim·§5.2 Three fixed pair experiments·inside propUpper score budget for pair experiments

Statement (paper)

After averaging over the fixed-base independent pair law restricted to distinct pairs, and over bases and places, the contribution of distinct pairs to DiD_i is at most O(1)+4δ2λ2(1/4−δ2)Ci≤O(1)+10δ2λCiO(1)+\frac{4\delta^2\lambda}{2(1/4-\delta^2)}C_i\le O(1)+10\delta^2\lambda C_i.

In plain English

After averaging over the fixed-base independent pair law restricted to distinct pairs, and over bases and places, the distinct-pair contribution to DiD_i is at most O(1)+4δ2λ2(1/4−δ2)CiO(1)+\frac{4\delta^2\lambda}{2(1/4-\delta^2)}C_i, which is at most O(1)+10δ2λCiO(1)+10\delta^2\lambda C_i.

Why it's here

The previous claim leaves window terms of size λ∣Jv∣\lambda|J_v|, charged only when both ne(v)n_e(v) and ne′(v)n_{e'}(v) lie in the interior of JvJ_v. The interval lemma's interior-mass bound makes each endpoint fall there with probability at most 2δ2\delta, so the pair event has probability at most 4δ24\delta^2. Normalizing by the pair law on distinct pairs gives the factor 1/(2(1/4−δ2))1/(2(1/4-\delta^2)), and this is at most 1010 once δ\delta is small. This yields the 10δ2λCi10\delta^2\lambda C_i term of the parent bound, with the O(1)O(1) constant absorbed into o(S)o(S).
Classified routine:
A direct probabilistic bookkeeping step. It combines the interval lemma's interior-mass bound (probability at most 2δ per endpoint, so 4δ² for the pair) with normalization by the distinct-pair law, and adds no new idea.

Uses

claimCentral-window excess and product-formula cancellationlemInterval overlap envelope and interior mass bound

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.2 Three fixed pair experiments
Page
—
Label
—
Line
sections/04-budgets.tex:367
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Averaging bounds distinct pairs by 10δ²λC_i" rests on claim-bud-upper-3
  • info
    inferred_dep
    outline: "Averaging bounds distinct pairs by 10δ²λC_i" rests on bud:intervals