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 are at least , and hence . Since , it follows that .
In plain English
Summing the slice-wise inequality gives . Because , this forces .
Why it's here
Averaging the slice-wise classification bound (claim-com-variation-2) against gives a lower bound of order on the score budget, with the slice errors totaling . The upper budget (bud-upper) bounds the same quantity by only . The two bounds are compatible only if the common contribution is , 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.
Uses
Used by
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
- infoinferred_depoutline: "Comparing budgets gives C_Q+C_Pθ=o(S)" rests on claim-com-variation-2