claimroutineinferred_dep

Small star variations force small f on common levels

Claim·§6.3 A second score forces positive rare mass·inside propRare point exceptions have positive mass

Statement (paper)

There is an absolute constant CC such that, uniformly for all sufficiently large tt, at every common level f≤C(VP+VQ)f\le C(V_P+V_Q), where VP,VQV_P,V_Q are the ordinary star variations at that level. Consequently ∫Cf≤C(CP+CQ)=o(S)\int_{\mathcal C}f\le C(C_P+C_Q)=o(S).

In plain English

For all sufficiently large tt, at every common level the minority-bit probability satisfies f≤C(VP+VQ)f\le C(V_P+V_Q), where VP,VQV_P,V_Q are the ordinary star variations at that level and CC is an absolute constant. Integrating over the common levels C\mathcal C gives ∫Cf≤C(CP+CQ)=o(S)\int_{\mathcal C}f\le C(C_P+C_Q)=o(S).

Why it's here

This is a pointwise comparison between ff and the star variations, which turns the negligibility of the common variations (from claim-com-rare-positive-3 for CPC_P and com:variation for CQC_Q) into smallness of ff integrated over common levels. It supplies the common-level part of the final argument in the next claim, which handles the remaining rare levels to reach the contradiction S=o(S)S=o(S).
Classified routine:
Direct application of the paper's inc-matching lemma at each common level, which gives f at most C times the star variations. Integrating and inserting the negligibility bounds from claim-com-rare-positive-3 and com-variation then yields o(S).

Uses

lemMatching labels are nearly constantclaimPoint-star common variation is negligiblepropCommon variation is negligible

Used by

claimRare levels also small, giving contradiction

Sources

PaperOpen
Section
§6.3 A second score forces positive rare mass
Page
—
Label
—
Line
sections/05-common-levels.tex:533
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Small star variations force small f on common levels" rests on claim-com-rare-positive-3
  • info
    inferred_dep
    outline: "Small star variations force small f on common levels" rests on com:variation