claimroutineinferred_dep

Floor and capacity exponents make sums converge

Choosing c1c_1, then c2c_2, then KnK_n makes every error series converge
combines all error terms into Cbufc∗2−pC_{\rm buf}c_*2^{-p}
Claim·§8.4 Charging overflow events·inside propCompression preserves row error budget

Statement (paper)

For c1>B1c_1>B_1 sufficiently large for the floor conditions and c2>sc1+sB1c_2>sc_1+sB_1 with a fixed positive margin and sufficiently large that nj≥Kn_j\geq K, the sum in Equation  converges uniformly, with mean-term exponential factor exactly 2−(c2−sc1−sB1)dj2^{-(c_2-sc_1-sB_1)d_j}. The outer sum in Equation  converges, its inner sum being at most C(dj+1)A2B1djC(d_j+1)^A2^{B_1d_j} for a fixed AA and its exponential factor being 2−((c2−c1)/s−B1)dj2^{-((c_2-c_1)/s-B_1)d_j}. For KnK_n sufficiently large the noise sum is controlled, and the preloss sum converges since c1>B1c_1>B_1, all with constants fixed before the choice of the small prefix coefficient c∗c_*.

In plain English

For c1>B1c_1>B_1 large enough for the floor conditions and c2>sc1+sB1c_2>sc_1+sB_1 with a fixed positive margin (and large enough that nj≥Kn_j\geq K), the false-type sum converges uniformly with factor 2−(c2−sc1−sB1)dj2^{-(c_2-sc_1-sB_1)d_j}. The true-type outer sum also converges, with inner sum at most C(dj+1)A2B1djC(d_j+1)^A2^{B_1d_j} and factor 2−((c2−c1)/s−B1)dj2^{-((c_2-c_1)/s-B_1)d_j}; the noise sum is controlled for large KnK_n and the preloss sum converges since c1>B1c_1>B_1.

Why it's here

This claim fixes c1c_1, then c2c_2, then KnK_n, so that the series bounds from the preloss, false-type, true-type mean and noise claims all converge. Their total is then bounded by a constant times c∗2−pc_*2^{-p}, with every constant fixed before the small prefix coefficient c∗c_* is chosen, which is what gives the integrated error bound of the proposition.
Classified routine:
Parameter bookkeeping: picking c1c_1, then c2c_2, then KnK_n so that the geometric series from the earlier preloss, false-type, true-type and noise claims (claims 2–5) converge. This is a standard exponent-comparison argument with no new idea.

Uses

claimPreloss and no-overflow error boundsclaimFalse-type first overflow charge boundclaimTrue-type overflow mean part via rarityclaimNoise part needs no sum over overflow groups

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-2
  • info
    inferred_dep
    outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-3
  • info
    inferred_dep
    outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-4
  • info
    inferred_dep
    outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-5