claimroutineinferred_dep

True-type overflow mean part via rarity

True-type overflow mean error gains

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

via rarity

true-type mean term of the error budget

Claim·§8.4 Charging overflow events·inside propCompression preserves row error budget

Statement (paper)

For true-type first overflow at

j

, after splitting

e_i\leq\beta_i+\gamma_i

via Lemma , the mean part (enlarging the actual first-overflow event to

\Theta_j

and using Equation and Minkowski's inequality) has total norm at most

Cc_*2^{-p}\sum_j(n_j\rho_j)^{-1/s}\sum_{i\geq j}C_1^{m_*-i+1}2^{B_1d_i}

In plain English

For a true-type first overflow at group

j

, the mean part of the error has total

L_s

norm at most

Cc_*2^{-p}\sum_j(n_j\rho_j)^{-1/s}\sum_{i\geq j}C_1^{m_*-i+1}2^{B_1d_i}

Why it's here

Splitting

e_i\leq\beta_i+\gamma_i

with the relative-stability lemma gives geometrically weighted per-group errors. The mean parts

\beta_i

are then masked by enlarging the actual first-overflow event to

\Theta_j

, so the rarity lemma yields the

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

gain, and Minkowski's inequality sums over

i

and

j

. This gives the true-type mean contribution in the charging argument, which is then summed in later claims using the floor and capacity exponent choices.

Classified routine:

Direct bookkeeping step: it combines the paper's relative-stability lemma and rarity/masking lemma with Minkowski's inequality to bound the mean part of the overflow error. No new idea is introduced beyond those earlier nodes.

Uses

lemRelative stability at first overflowlemBuffer overflow events are rare

Used by

claimFloor and capacity exponents make sums converge

Sources

PaperOpen

Section: §8.4 Charging overflow events
Page: —
Label: —
Line: sections/compression.tex:508

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "True-type overflow mean part via rarity" rests on lem:buf-rarity