lemmaroutine

Omitting one fine bin costs little

Omitting one fine bin costs norm at most C(b/a)(s−1)/sC(b/a)^{(s-1)/s}
per-bin omission cost summed in the mean-prefix bound
Lemma·lem:est-omission·§7.3 Mean comparisons and the cost of releasing a source

Statement (paper)

If one fine bin is omitted, the norm of its normalized contribution is at most C(b/a)(s−1)/sC(b/a)^{(s-1)/s}. This applies to direct terms, routed terms, and correction--bin products.

In plain English

If a single fine bin is omitted, the norm of its normalized contribution is at most C(b/a)(s−1)/sC(b/a)^{(s-1)/s}. This bound holds for direct terms, routed terms, and correction–bin products alike.

Why it's here

This is the basic per-bin omission estimate that later mean-comparison arguments sum over omitted bins. For correction–bin products it relies on the bounded row sums and entries from the correction–bin product lemma, whose constants do not depend on the bin scale bb, so one bound covers all three kinds of terms. The mean-prefix lemma uses it to control the cost of dropping bins.
Classified routine:
A direct per-bin norm estimate obtained from the bounded row sums and entries in the correction–bin product lemma (lem-hier-bin-products). It combines them by a standard Hölder/interpolation-type bound between row-sum and entry bounds, which yields the exponent (s-1)/s.

Uses

lemCorrection-bin products have bounded size

Used by

lemMean prefixes are small against targets

Sources

PaperOpen
Section
§7.3 Mean comparisons and the cost of releasing a source
Page
—
Label
lem:est-omission
Line
sections/estimation.tex:333
Leannot aligned

Phase 2 aligns this node to a Lean declaration.