claimroutineinferred_dep
Ordered approximations with error and time bounds
Approximating costs with error
arithmetic cost and error of the factors
Statement (paper)
There are ordered-coordinate algorithms for , , with errors at most , , and times , , respectively. The selection map (selecting coordinates with , , ) is computed exactly, with zero numerical error, in time . Hence and have errors less than and respectively, and the total cost is .
In plain English
The scaled maps , , have ordered-coordinate algorithms with errors at most , , and times , , , and the coordinate selection is computed exactly in time . Hence and have errors below and total cost .
Why it's here
This turns the exact factorization , into the fixed multitape algorithms the lemma requires. Since adds no numerical error, the errors of the composed maps are the sum of those of the factors, and each stays below . The time bounds of the factors add up to the lemma's , apart from the tape-movement accounting, which is handled in a later claim.
Classified routine:
Error and cost bookkeeping that combines the earlier bounds for the factor maps S', J', D' with the standard rule that errors add under composition of contractions, adapting the resampling error analysis of Harvey–van der Hoeven (2021). The coordinate selection C is just exact copying of entries.
Uses
Used by
Sources
PaperOpen
- Section
- §8.1 The one-dimensional interface
- Page
- —
- Label
—- Line
sections/07-resampling.tex:149
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Ordered numerical maps and selection error bounds" rests on claim-lem-no-sort-resampling-1