lemmaroutine
Correction-bin products have bounded size
Correction–bin products have row sums ≤ , entries ≤ , ≤
scale-free product bounds for omission estimates
Lemma·
lem:hier-bin-products·§5.2 Dense bins and preparatory normalizationStatement (paper)
Let be the transition matrix at the current stage, and let be
any finite pilot or actual correction there. If a matrix
on the same vertex set satisfies and
for some , then
If also , then . These estimates have constants
independent of the bin scale .
In plain English
For a finite pilot or actual correction and a nonnegative matrix with row sums at most 1 and entries at most , the product has row sums at most and entries at most . If also , then . The constants do not depend on the bin scale .
Why it's here
This turns the pilot and actual bounds (row sums at most ) into row-sum and entry bounds for products of a correction with a bin matrix, using only that has bounded row sums and is substochastic with small entries. Because the constants do not depend on , later omission estimates can apply it to correction–bin products at every bin scale, and the comparison lets such products be dominated by the full product .
Classified routine:
A direct consequence of the row-sum bounds in the pilot-bounds lemma together with elementary nonnegative matrix inequalities: row sums multiply, entries are bounded by (row sum of F) times (max entry of A_b), and monotonicity follows from F being nonnegative.
Sources
PaperOpen
- Section
- §5.2 Dense bins and preparatory normalization
- Page
- —
- Label
lem:hier-bin-products- Line
sections/atoms.tex:264
Leannot aligned
Phase 2 aligns this node to a Lean declaration.