lemmaroutine

Buffer update map: replacement, monotonicity, Lipschitz

Buffer update replaces small entries, keeps large ones, and is Lipschitz
basic properties of the compression step
Lemma·lem:buf-update·§8.2 The update map

Statement (paper)

The update has the following properties. It replaces every position of size at most 2u02u_0 by the new default, is identity at every position of size at least 3u03u_0, and lies coordinatewise between the input and the new default. The default is nondecreasing. The map from the input array and old default to the updated array and new default is uniformly Lipschitz in the sup norm. A list containing all exceptions can be chosen with at most njn_j positions, using only the previous list and the new candidates.

In plain English

The buffer update replaces every array position of size at most 2u02u_0 by the new default, leaves every position of size at least 3u03u_0 unchanged, and keeps the result coordinatewise between the input and the new default. The default is nondecreasing, the map from (input array, old default) to (updated array, new default) is uniformly Lipschitz in the sup norm, and a list containing all exceptions can be chosen with at most njn_j positions using only the previous list and the new candidates.

Why it's here

This lemma collects the basic properties of the update step that later buffer arguments rely on. Replacement below 2u02u_0, identity above 3u03u_0, and sandwiching between input and default control what the update can change. Lipschitz continuity lets discrepancies propagate through the update with bounded loss, and the njn_j bound keeps the exception list small.
Classified routine:
Direct verification of elementary properties (thresholding at 2u02u_0/3u03u_0, sandwiching, monotone default, sup-norm Lipschitz bound, exception-list counting) of the paper's own buffer update map. It amounts to bookkeeping and uses no other results.

Uses

Nothing else in the paper

Used by

lemRelative stability at first overflowlemDirect collision charge boundlemEstimator recipes have regenerable records and bounded controlclaimSentinel modification gives Lipschitz propagation boundclaimPropagated clean height has small row normclaimRanks, compression and list selection

Sources

PaperOpen
Section
§8.2 The update map
Page
—
Label
lem:buf-update
Line
sections/compression.tex:159
Leannot aligned

Phase 2 aligns this node to a Lean declaration.