claimroutineinferred_dep

Common variation is negligible by budget comparison

Claim·§6.2 Classification and suppression of common variation·inside propCommon variation is negligible

Statement (paper)

The common contributions to DQ+DPθD_Q+D_{P\theta} are at least λ4(CQ+CPθ)−o(S)\frac\lambda4(C_Q+C_{P\theta})-o(S), and hence λ4(CQ+CPθ)−o(S)≤DQ+DPθ≤10δ2λ(CQ+CPθ)+o(S)\frac\lambda4(C_Q+C_{P\theta})-o(S)\le D_Q+D_{P\theta}\le 10\delta^2\lambda(C_Q+C_{P\theta})+o(S). Since 10δ2<1/410\delta^2<1/4, it follows that CQ+CPθ=o(S)C_Q+C_{P\theta}=o(S).

In plain English

Summing the slice-wise inequality gives λ4(CQ+CPθ)−o(S)≤DQ+DPθ≤10δ2λ(CQ+CPθ)+o(S)\frac\lambda4(C_Q+C_{P\theta})-o(S)\le D_Q+D_{P\theta}\le 10\delta^2\lambda(C_Q+C_{P\theta})+o(S). Because 10δ2<1/410\delta^2<1/4, this forces CQ+CPθ=o(S)C_Q+C_{P\theta}=o(S).

Why it's here

Averaging the slice-wise classification bound (claim-com-variation-2) against πθ\pi_\theta gives a lower bound of order λ(CQ+CPθ)\lambda(C_Q+C_{P\theta}) on the score budget, with the slice errors totaling o(S)o(S). The upper budget (bud-upper) bounds the same quantity by only 10δ2λ(CQ+CPθ)+o(S)10\delta^2\lambda(C_Q+C_{P\theta})+o(S). The two bounds are compatible only if the common contribution is o(S)o(S), which is the first half of the proposition and feeds into the comparison of rare exception means in the next claim.
Classified routine:
A direct combination of the slice-wise lower bound (claim-com-variation-2), averaged over template slices, with the upper score budget (bud-upper); the conclusion is a simple comparison of constants, using 10δ²<1/4.

Sources

PaperOpen
Section
§6.2 Classification and suppression of common variation
Page
—
Label
—
Line
sections/05-common-levels.tex:329
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Comparing budgets gives C_Q+C_Pθ=o(S)" rests on claim-com-variation-2