claimroutineinferred_dep

Failure forces small exceptions and small T

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

Statement (paper)

If fails, then along a subsequence EμHp∗=o(S)\E_\mu H_p^*=o(S), and consequently EκHq∗=o(S)\E_\kappa H_q^*=o(S) and T≤o(S)T\le o(S).

In plain English

If the liminf of EμHp∗/S\E_\mu H_p^*/S were zero, then along a subsequence EμHp∗=o(S)\E_\mu H_p^*=o(S), which gives EκHq∗=o(S)\E_\kappa H_q^*=o(S) and T≤o(S)T\le o(S).

Why it's here

This sets up the proof by contradiction for the proposition. The bound on the center exceptions follows from the comparison EκHq∗≤EμHp∗+o(S)\E_\kappa H_q^*\le\E_\mu H_p^*+o(S) in the common-variation proposition, and the bound on TT follows from the prediction-score lemma. The later claims then work under these smallness assumptions.
Classified routine:
Direct consequence of the earlier nodes: negating the liminf statement gives a subsequence with E_mu H_p^* = o(S). The center bound then follows from the comparison in the common-variation proposition, and the bound on T from the prediction-score lemma.

Uses

lemSmall rare exceptions force small prediction scorepropCommon variation is negligible

Used by

claimPointwise point-star slice inequality

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Assumption forces center exceptions and T small" rests on com:variation