claimroutineinferred_dep

Center rare exceptions bounded by point ones

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

Statement (paper)

EκHq∗≤EμHp∗+o(S)\E_\kappa H_q^*\le\E_\mu H_p^*+o(S), i.e., the rare exception mean of the center-star experiment is at most that of the point--template-star experiment up to an error o(S)o(S).

In plain English

The rare exception mean EκHq∗\E_\kappa H_q^* of the center-star experiment is at most the rare exception mean EμHp∗\E_\mu H_p^* of the point--template-star experiment, up to an error o(S)o(S).

Why it's here

Since the previous claim gives CQ+CPθ=o(S)C_Q+C_{P\theta}=o(S), the upper budget (bud-upper) makes the score of the QQ experiment o(S)o(S). The rare-exception lower bound (bud-rare-lower) says this score is at least 2EκHq∗−2EμHp∗−o(S)2\E_\kappa H_q^*-2\E_\mu H_p^*-o(S), and combining the two gives the stated comparison, which is the second half of the proposition.
Classified routine:
Direct consequence of earlier nodes: substitute CQ+CPθ=o(S)C_Q+C_{P\theta}=o(S) from the previous claim into the upper budget (bud-upper), then compare with the rare-exception lower bound (bud-rare-lower).

Uses

propRare-exception lower bound on pair scorespropUpper score budget for pair experimentsclaimCommon variation is negligible by budget comparison

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Center rare exceptions bounded by point ones" rests on claim-com-variation-3