claimroutineinferred_dep

Preloss and no-overflow error bounds

Preloss and no-overflow errors are at most Cc∗2−p∑ρi(⋯ )Cc_*2^{-p}\sum\rho_i(\cdots)
preloss and no-overflow terms of the error budget
Claim·§8.4 Charging overflow events·inside propCompression preserves row error budget

Statement (paper)

The preloss contributions have norm at most Cc∗2−p∑iρi(2B1di+2−Kndi)Cc_*2^{-p}\sum_i\rho_i\bigl(2^{B_1d_i}+2^{-K_nd_i}\bigr). On the event of no overflow, the final-prefix cost adds at most Cc∗2−p(2B1+2−Kn)Cc_*2^{-p}(2^{B_1}+2^{-K_n}).

In plain English

The error contributions from losses incurred before an overflow have norm at most Cc∗2−p∑iρi(2B1di+2−Kndi)Cc_*2^{-p}\sum_i\rho_i(2^{B_1d_i}+2^{-K_nd_i}). On the event of no overflow, the final-prefix cost adds at most Cc∗2−p(2B1+2−Kn)Cc_*2^{-p}(2^{B_1}+2^{-K_n}).

Why it's here

This claim handles the part of the integrated error budget coming from pre-overflow loss and from runs that never overflow. It compares with the stationary reference calculation of the buffer-reference lemma, whose root outputs are within C∑iρieiC\sum_i\rho_i e_i of the true ones, and uses the row-sup-to-summed-power conversion to get a norm bound. The resulting bounds feed the later choice of floor and capacity exponents, so the sums converge.
Classified routine:
A direct bookkeeping consequence of the pre-overflow reference bound (lem-buf-reference) combined with the row-sup-to-summed-power conversion (claim-prop-buf-error-1); it only sums the per-group losses against the fixed weights.

Uses

lemPre-overflow buffer loss and reference calculationclaimRow sup bounds convert to summed powers

Used by

claimFloor and capacity exponents make sums converge

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Preloss and no-overflow contributions" rests on lem:buf-reference
  • info
    inferred_dep
    outline: "Preloss and no-overflow contributions" rests on claim-prop-buf-error-1