claimroutine

Row sup bounds convert to summed powers

Row sup bounds convert to summed

s

-th powers at fixed factor

converts sup bounds into the summed-power norm

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

Statement (paper)

Equation converts every row sup bound into a bound for the summed output power with a fixed factor: the support of a discrepancy lies in the union of the true and computed supports, whose total size over

\mathcal H

is at most

2C_{\mathrm{supp}}

, so this step introduces no factor from the ambient number of endpoints.

In plain English

A uniform bound on each row's discrepancy (the row support bound) yields a bound on the sum over

H\in\mathcal H

and

y

of the discrepancy's

s

-th power. This costs only a fixed factor, because a discrepancy is supported on the union of the true and computed supports, whose total size over

\mathcal H

is at most

2C_{\mathrm{supp}}

Why it's here

This turns pointwise row sup bounds into the summed-power norm that the integrated error bound for the proposition uses. The conversion depends only on the support size

2C_{\mathrm{supp}}

and not on the ambient number of endpoints, so

C_{\mathrm{buf}}

stays independent of the number of groups and row width. The later claims on preloss, no-overflow and overflow contributions use it to convert their sup bounds into summed powers.

Classified routine:

An elementary sup-to-sum bound: summing the s-th power of a function bounded pointwise over a support of size at most 2C_supp gives at most 2C_supp times the sup to the s-th power. It is bookkeeping inside the paper's own buffer-error argument.

Uses

Nothing else in the paper

Used by

claimPreloss and no-overflow error boundsclaimFalse-type first overflow charge bound

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.