claimroutineinferred_dep

Tape movement and Neumann iteration bounds

Tape movement and Neumann iteration fit in

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

closes the time bound of the resampling lemma

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

Statement (paper)

The remaining tape movement inside the quoted algorithms satisfies the claimed bound

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

. In particular, with

E=N-I

and

k=\lceil p/(\alpha^2\theta)\rceil

, every iterate

\widetilde v^{(j)}

of the Neumann evaluation lies in

\mathbb D_p^s

and all computed partial sums are

O(p)

-bit records. The

\mathsf S'

window scans, the

k-1

calls of

\widetilde E

with their row additions, and the outer accumulation together cost

O(tp\sqrt p\,\alpha)

, with the tape count and constants uniform in

p,s,t,\alpha

In plain English

The tape movement left over in the algorithms for

\widetilde A

and

\widetilde B_0

costs

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

. With

E=N-I

and

k=\lceil p/(\alpha^2\theta)\rceil

, every Neumann iterate

\widetilde v^{(j)}

lies in

\mathbb D_p^s

, all partial sums are

O(p)

-bit records, and the

\mathsf S'

window scans, the

k-1

calls of

\widetilde E

with row additions, and the outer accumulation together cost

O(tp\sqrt p\,\alpha)

Why it's here

This finishes the time bound of the parent lemma. The earlier claim bounded the arithmetic cost of the factors but left tape movement open. Here the number of Neumann terms

k

is controlled via

\theta>p/\alpha^4

, so the iteration and its bookkeeping fit within

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

with constants uniform in

p,s,t,\alpha

Classified routine:

Direct bookkeeping of tape movement and the Neumann-series iteration count, using the earlier claim's error and time bounds for the scaled maps together with the condition θ > p/α^4; no new idea beyond standard cost accounting.

Uses

claimOrdered approximations with error and time bounds

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Tape movement and Neumann iteration bounds" rests on claim-lem-no-sort-resampling-2