claimroutineinferred_dep

Noise part needs no sum over overflow groups

True-type overflow noise error needs no sum over overflow groups
true-type noise term of the error budget
Claim·§8.4 Charging overflow events·inside propCompression preserves row error budget

Statement (paper)

Since on each row at most one first-overflow event Oj\mathcal O_j occurs, ∑j1Oj∑i≥jC1m∗−i+1γi≤∑iC1m∗−i+1γi\sum_j\mathbf1_{\mathcal O_j}\sum_{i\geq j}C_1^{m_*-i+1}\gamma_i\leq\sum_iC_1^{m_*-i+1}\gamma_i pointwise, regardless of dependence between noise and overflow. Hence, by the absolute prefix-noise bound, the noise part of the true-type first-overflow error has norm at most Cc∗2−p∑iC1m∗−i+12−KndiCc_*2^{-p}\sum_iC_1^{m_*-i+1}2^{-K_nd_i}, without an extra sum over jj.

In plain English

Because each row has at most one first-overflow event Oj\mathcal O_j, the indicator-weighted noise sum is pointwise at most ∑iC1m∗−i+1γi\sum_iC_1^{m_*-i+1}\gamma_i, whatever the dependence between noise and overflow. So the noise part of the true-type first-overflow error has norm at most Cc∗2−p∑iC1m∗−i+12−KndiCc_*2^{-p}\sum_iC_1^{m_*-i+1}2^{-K_nd_i}, with no extra sum over jj.

Why it's here

Relative stability gives an error of the form ∑i≥jC1m∗−i+1ei\sum_{i\geq j}C_1^{m_*-i+1}e_i once overflow first occurs in group jj. Since the events Oj\mathcal O_j are disjoint on each row, summing over jj costs nothing extra. No independence between noise and overflow is needed, and the noise contribution stays a single geometric sum that the later convergence step can control.
Classified routine:
Follows from the disjointness of the first-overflow events on each row: the indicator-weighted sum is pointwise bounded by the full sum. Combined with the earlier relative-stability lemma and the absolute prefix-noise bound, this is simple bookkeeping.

Uses

lemRelative stability at first overflow

Used by

claimFloor and capacity exponents make sums converge

Sources

PaperOpen
Section
§8.4 Charging overflow events
Page
—
Label
—
Line
sections/compression.tex:518
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Noise part via uniqueness of first overflow" rests on lem:buf-relative-stability