lemmaroutine

Interval overlap envelope and interior mass bound

Lemma·bud:intervals·§5.2 Three fixed pair experiments

Statement (paper)

Let b≤b′b\le b', T≥0T\ge0, and JJ be an interval of finite length, with any choice of included endpoints. Put I−=[b−T,b]I_-=[b-T,b], I+=[b′,b′+T]I_+=[b',b'+T], and a=∣J∩I−∣+∣J∩I+∣a=|J\cap I_-|+|J\cap I_+|, where ∣⋅∣|\cdot| denotes length. For 0<λ<10<\lambda<1, [(1−λ)2T+2λa−2T]+≤λ∣J∣ 1{b,b′∈int⁡J}. \big[(1-\lambda)2T+2\lambda a-2T\big]_+ \le\lambda|J|\, \mathbf1_{\{b,b'\in\operatorname{int}J\}}. If XX has any probability law on R\R, and ∣P(X>s)−1/2∣≤δ|\Prob(X>s)-1/2|\le\delta throughout JJ, then P(X∈int⁡J)≤2δ. \Prob(X\in\operatorname{int}J)\le2\delta.

In plain English

For intervals I−=[b−T,b]I_-=[b-T,b] and I+=[b′,b′+T]I_+=[b',b'+T] and an interval JJ with a=∣J∩I−∣+∣J∩I+∣a=|J\cap I_-|+|J\cap I_+|, the excess [(1−λ)2T+2λa−2T]+[(1-\lambda)2T+2\lambda a-2T]_+ is at most λ∣J∣\lambda|J| when both b,b′b,b' lie in the interior of JJ, and is 00 otherwise. Also, if P(X>s)\Prob(X>s) stays within δ\delta of 1/21/2 throughout JJ, then XX lies in the interior of JJ with probability at most 2δ2\delta.

Why it's here

This is an elementary tool for the upper score budget. The first part caps the gain from the two windows I±I_\pm by λ∣J∣\lambda|J|, and only when both centers b,b′b,b' lie inside JJ. The second part bounds the probability of that event by 2δ2\delta, since the tail probability varies by at most 2δ2\delta across JJ and so the interior mass is small.
Classified routine:
Elementary interval-length and tail-probability bookkeeping: the envelope follows from a ≤ T plus overlap considerations, and the interior-mass bound is the difference of two tail probabilities that each lie within δ of 1/2. It is a self-contained helper for the score budget, not a new idea.

Uses

Nothing else in the paper

Used by

propUpper score budget for pair experimentsclaimCentral-window excess and product-formula cancellationclaimAveraging bounds distinct-pair budget by 10δ²λC_i

Figures

A horizontal axis labeled $s$ carries tick marks at $b-T$, $b$, $b'$, $b'+T$. Above the axis, two light-blue shaded bands with dark blue lines mark the flanking intervals $I_-=[b-T,b]$ and $I_+=[b',b'+T]$, separated by a gray band labeled "different bits" over $[b,b']$. Below the axis, an orange bracketed segment labeled "central window $J$" starts inside $I_-$ and ends inside $I_+$, with dotted vertical lines showing that $b$ and $b'$ both lie in its interior. It illustrates that a window whose overlap with the two flanks exceeds $T$ must contain both thresholds strictly inside.
Figure 1schematicp. 26
The intervals I−=[b−T,b]I_-=[b-T,b] and I+=[b′,b′+T]I_+=[b',b'+T], with b≤b′b\le b' and T≥0T\ge0, flank the bit-difference interval. The central window JJ in creates excess only if its total overlap with the two flanks exceeds TT; then both thresholds lie strictly inside JJ.
What it shows
A horizontal axis labeled ss carries tick marks at b−Tb-T, bb, b′b', b′+Tb'+T. Above the axis, two light-blue shaded bands with dark blue lines mark the flanking intervals I−=[b−T,b]I_-=[b-T,b] and I+=[b′,b′+T]I_+=[b',b'+T], separated by a gray band labeled "different bits" over [b,b′][b,b']. Below the axis, an orange bracketed segment labeled "central window JJ" starts inside I−I_- and ends inside I+I_+, with dotted vertical lines showing that bb and b′b' both lie in its interior. It illustrates that a window whose overlap with the two flanks exceeds TT must contain both thresholds strictly inside.
Read from the image by claude-opus-5.5 · confidence 85%
SupportslemInterval overlap envelope and interior mass boundclaimPlace identity and flanking positive-charge intervalsclaimCentral-window excess and product-formula cancellation

Sources

PaperOpen
Section
§5.2 Three fixed pair experiments
Page
—
Label
bud:intervals
Line
sections/04-budgets.tex:244
Leannot aligned

Phase 2 aligns this node to a Lean declaration.