claimroutine

Record format conversions are cheap and exact

Record format conversions are exact and cost

O(tp)

shows format bookkeeping is negligible

Claim·§8.1 The one-dimensional interface·inside lemOne-dimensional resampling without sorting

Statement (paper)

The conversions between the scalar record format of the cited numerical routines (sign symbol, binary magnitude, separators, real field before imaginary field, pairs in coordinate order) and the

w_{\rm c}

-bit word format used here are performed by fixed multitape algorithms that preserve every represented integer and hence add no error. Each conversion takes

O(p)

time, including preparation of the unary ruler of

w_{\rm c}

cells, so on Gaussian line lengths

s<t

they cost

O((s+t)p)=O(tp)

, and

O(p)

per exponential output, which is within the stated bound

O(tp^{3/2+\delta}\alpha)

In plain English

Converting between the scalar record format of the cited numerical routines and the

w_{\rm c}

-bit word format used here is done by fixed multitape algorithms that preserve every represented integer, so they add no error. Each conversion takes

O(p)

time, so on lines of lengths

s<t

the total cost is

O((s+t)p)=O(tp)

Why it's here

This claim handles the bookkeeping in the proof of the lemma: the cited routines and the word-based algorithms use different encodings, and the claim shows that translating between them neither changes values nor costs much. Its

O(tp)

total, together with

O(p)

per exponential output, is well within the stated

O(tp^{3/2+\delta}\alpha)

bound, so the conversions can be ignored in the final time and error accounting.

Classified routine:

Standard Turing-machine bookkeeping: converting between two fixed integer encodings by a linear scan costs O(p) per record and is exact. Summing over the s+t records of a Gaussian line gives O(tp), which is far below the lemma's O(tp^{3/2+δ}α) bound.

Uses

Nothing else in the paper

Used by

Nothing in the paper

Sources

PaperOpen

Section: §8.1 The one-dimensional interface
Page: —
Label: —
Line: sections/07-resampling.tex:203

Leannot aligned

Phase 2 aligns this node to a Lean declaration.