lemmaroutine

Rare exceptions: comparison, first moments, joint bounds

Lemma·bud:rare-moments·§5.1 Parameters, rare levels, and histories

Statement (paper)

Uniformly on G\mathcal G, hP+hQ≤C(f+m)=o(1),f≤hP+hQ+m. h_P+h_Q\le C(f+m)=o(1),\qquad f\le h_P+h_Q+m. Consequently EμHp∗+EκHq∗=O(S). \E_\mu H_p^*+\E_\kappa H_q^*=O(S). Furthermore, with (p,q,r)(p,q,r) the ordinary wedge law, ∫GPE(Ip=Iq=1)=o(S),∫GP(Ip=Ir=1)=o(S). \int_{\mathcal G}\Prob_E(I_p=I_q=1)=o(S),\qquad \int_{\mathcal G}\Prob(I_p=I_r=1)=o(S).

In plain English

Uniformly on G\mathcal G, the rare-set masses satisfy hP+hQ≤C(f+m)=o(1)h_P+h_Q\le C(f+m)=o(1) and f≤hP+hQ+mf\le h_P+h_Q+m, so EμHp∗+EκHq∗=O(S)\E_\mu H_p^*+\E_\kappa H_q^*=O(S). Under the ordinary wedge law, the joint exception events satisfy ∫GPE(Ip=Iq=1)=o(S)\int_{\mathcal G}\Prob_E(I_p=I_q=1)=o(S) and ∫GP(Ip=Ir=1)=o(S)\int_{\mathcal G}\Prob(I_p=I_r=1)=o(S).

Why it's here

This lemma ties the rare-level masses hP,hQh_P,h_Q to the minority-bit probability ff and the mass mm, which gives a first-moment bound of order SS on the exception counts. Applying the rare-set edge-mass bound (inc-rare) to the exception sets shows that simultaneous exceptions at two vertices of an edge or wedge are o(S)o(S). The budget, positivity and profile arguments that use it can therefore treat the exceptions as a single-vertex effect of size O(S)O(S) with negligible joint contribution.
Classified routine:
This is bookkeeping that compares the rare-level masses with the minority-bit probability and then sums to get first moments. The joint bounds follow directly by applying the earlier rare-set edge-mass lemma (inc-rare) to the exception sets.

Uses

lemRare sets carry little edge mass

Used by

propUpper score budget for pair experimentspropRare-exception lower bound on pair scorespropRare point exceptions have positive masslemPoint profiles approximate wedge differencesclaimEqual-endpoint collisions contribute o(S)claimRare levels also small, giving contradiction

Sources

PaperOpen
Section
§5.1 Parameters, rare levels, and histories
Page
—
Label
bud:rare-moments
Line
sections/04-budgets.tex:82
Leannot aligned

Phase 2 aligns this node to a Lean declaration.