lemmaroutine

Raw difference bounds at slack-d groups

Slack-dd raw differences are at most 2−p+O(d)2^{-p+O(d)} times child discrepancies
cheap 2O(d)2^{O(d)} loss estimate for prefix and coupling steps
Lemma·lem:est-raw-difference·§7.6 Absolute difference bounds and averaging noise

Statement (paper)

At a slack-dd group, the ordinary raw norm of an unaveraged paired difference is at most CCb 2−p−A∗+C0d, C C_b\,2^{-p-A_*+C_0d}, where C0C_0 is fixed independently of the walk length coefficient. For two coupled versions of a budget-rr sample term, if the corresponding child discrepancies are bounded by 2−pr′λr2^{-p'_r}\lambda_r, their normalized raw difference is bounded by 2−p+C0′dλr2^{-p+C_0'd}\lambda_r, summed over the finitely many child types. For a paired layer at budgets mm and m−1m-1, apply this estimate to both parts. Its coupled discrepancy is consequently bounded by 2−p+C0′d(λm+λm−1)2^{-p+C_0'd}(\lambda_m+\lambda_{m-1}), after enlarging the fixed constant, or by the corresponding maximum over all children in the group. Every child in either part has budget at most M−dM-d. For a fixed guessed measure-preserving variant and its valid endpoint restriction the same bounds hold. Counting all variants separately may increase C0′C_0' by a constant depending on the chosen walk length.

In plain English

At a slack-dd group, the ordinary raw norm of an unaveraged paired difference is at most CCb2−p−A∗+C0dC C_b 2^{-p-A_*+C_0 d}. For coupled budget-rr sample terms whose child discrepancies are at most 2−pr′λr2^{-p'_r}\lambda_r, the normalized raw difference is at most 2−p+C0′dλr2^{-p+C_0'd}\lambda_r, summed over child types; for a paired layer at budgets mm and m−1m-1 the coupled discrepancy is at most 2−p+C0′d(λm+λm−1)2^{-p+C_0'd}(\lambda_m+\lambda_{m-1}), and all children have budget at most M−dM-d.

Why it's here

It packages the explicit scale-ratio and release costs from the mean comparison lemma into one raw-difference estimate that later prefix and collision-charging arguments can cite. The loss is only 2O(d)2^{O(d)} in precision, and the same bounds hold for guessed measure-preserving variants and valid endpoint restrictions, with a constant depending on the walk length when variants are counted separately.
Classified routine:
Repackages the scale-factor and release-cost bounds of the mean comparison lemma (lem-est-mean-comparison) into a single raw-difference estimate. This is done by bookkeeping over finitely many child types and both parts of a paired layer, with the constant enlarged to absorb the losses.

Uses

lemMean comparison scale factors and release cost

Used by

lemMean prefixes small, noise prefixes tinylemEscape contribution charged to child discrepancieslemDirect collision charge boundclaimPrecision gain absorbs scale and reset costsclaimCrude bound on clean group incrementsclaimRemaining terms bounded by child discrepancies

Sources

PaperOpen
Section
§7.6 Absolute difference bounds and averaging noise
Page
—
Label
lem:est-raw-difference
Line
sections/estimation.tex:605
Leannot aligned

Phase 2 aligns this node to a Lean declaration.