lemmaroutine

Buffer overflow events are rare

Overflow

\Theta_j

has conditional probability at most

C/(n_j\rho_j)

rarity input for charging overflow errors

Lemma·lem:buf-rarity·§8.4 Charging overflow events

Statement (paper)

At every specified endpoint,

\mathbb P(\Theta_j\mid X_u(x)=Y_a(y)=1) \leq\frac{C}{n_j\rho_j}.

The same bound holds with the narrower endpoint condition

Y_t(y)=1

. Moreover, for every prefix mean row supremum,

\|\mathbf1_{\Theta_j}\beta_i\|_{L_s(\mu)} \leq Cc_*2^{-p+B_1d_i}(n_j\rho_j)^{-1/s}.

In plain English

Conditioned on the specified endpoint events (such as

X_u(x)=Y_a(y)=1

, or the narrower

Y_t(y)=1

), the overflow event

\Theta_j

has probability at most

C/(n_j\rho_j)

. Consequently, masking a prefix mean row supremum

\beta_i

\mathbf 1_{\Theta_j}

gives

L_s(\mu)

norm at most

Cc_*2^{-p+B_1d_i}(n_j\rho_j)^{-1/s}

Why it's here

This is the rarity input for the overflow-charging argument: because

\Theta_j

is unlikely even given endpoint conditioning, the mean part of the true-type first-overflow error can be bounded by enlarging the actual first-overflow event to

\Theta_j

. The norm bound follows from the probability bound by Hölder, which yields the

(n_j\rho_j)^{-1/s}

gain. The conditioning on retained endpoints is handled with the pair-retention estimates of the rank channel lemma, which only inflate probabilities by constant factors.

Classified routine:

Follows from the rank-channel retention estimates (lem-env-ranks) by a Markov/counting bound on the overflow event, then Hölder's inequality to convert the probability bound into the masked

L_s

norm bound; standard bookkeeping within the paper's overflow-charging argument.

Uses

lemRank channel retention estimates

Used by

claimTrue-type overflow mean part via rarity

Sources

PaperOpen

Section: §8.4 Charging overflow events
Page: —
Label: lem:buf-rarity
Line: sections/compression.tex:411

Leannot aligned

Phase 2 aligns this node to a Lean declaration.