propositionroutineinferred_dep

Rare point exceptions have positive mass

Proposition·com:rare-positive·§6.3 A second score forces positive rare mass

Statement (paper)

The good rare point exceptions satisfy lim inf⁡t→∞EμHp∗S>0. \liminf_{t\to\infty}\frac{\E_\mu H_p^*}{S}>0.

In plain English

The expected good rare point exceptions EμHp∗\E_\mu H_p^* are bounded below by a positive constant multiple of SS as t→∞t\to\infty, that is, lim inf⁡t→∞EμHp∗/S>0\liminf_{t\to\infty}\E_\mu H_p^*/S>0.

Why it's here

The proof is by contradiction. If the liminf were zero, the prediction-score lemma and the common-variation comparison would make the center exceptions and TT small. The point-star and center-star variations would then be negligible on common levels, and the rare levels would be negligible too, forcing S=o(S)S=o(S). The positive lower bound on rare mass is what the later arguments, such as the band of accurate wedges, rely on.
Classified routine:
A contradiction argument that combines the paper's earlier lemmas: the prediction-score lemma, the common-variation comparison and the rare-exception lower bounds, which together force S=o(S)S=o(S). It is internal bookkeeping on top of those nodes rather than a new idea.

Uses

lemSmall rare exceptions force small prediction scorepropRare-exception lower bound on pair scoreslemMatching labels are nearly constantlemRare exceptions: comparison, first moments, joint boundspropCommon variation is negligible

Used by

lemCommon height band of accurate wedges

Inside the proof

claimFailure forces small exceptions and small TclaimPointwise point-star slice inequalityclaimPoint-star common variation is negligibleclaimSmall star variations force small f on common levelsclaimRare levels also small, giving contradiction

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    "As before, a pair with a bad slot costs only O(b_p)" and "The strict-cross classification proves the claim" point back to the classification of common variation in §6.2.