claimroutine

Axis exposure costs via chunk swaps

Exposing and restoring axes costs

O(Tp\,d^2(1+\ell^\tau))

via chunk swaps

bounds data movement for linewise algorithms

Claim·§8.2 Growing dimension and the padded array·inside lemTensor resampling across d dimensions

Statement (paper)

Under the stated assumptions (

t_i\in\{r/2,r\}

r=2^\ell

, the array kept in the full padded box of

T

entries, each entry occupying

O(p)

bits), each adjacent interchange of the

\ell

-bit or

(\ell-1)

-bit address fields of two axes costs

O(Tp(1+\ell^\tau))

, using Lemma for equal widths and, for unequal widths, an interchange of equal-width pieces together with a single bit move via Lemma . Exposing and restoring one axis needs

O(d)

adjacent interchanges, so all axes need

O(Tp\,d^2(1+\ell^\tau))

in total; these are exact permutations of the padded box and change neither norms nor errors.

In plain English

When each

t_i\in\{r/2,r\}

with

r=2^\ell

and the array is kept in the padded box of

T

entries of

O(p)

bits, swapping the address fields of two adjacent axes costs

O(Tp(1+\ell^\tau))

. Exposing and restoring every axis takes

O(d)

such swaps per axis, so

O(Tp\,d^2(1+\ell^\tau))

in total, and these are exact permutations that change neither norms nor errors.

Why it's here

This is the cost accounting for the data movement in the parent lemma: the linewise one-dimensional algorithms need each axis made contiguous, and this bounds that rearrangement. Equal-width fields are swapped with the chunk-swap lemma. When widths differ by one bit (

\ell

versus

\ell-1

), an equal-width swap plus one bit move from the elementary-streams lemma suffices, giving the

d^2

factor from

O(d)

swaps for each of the

d

axes.

Classified routine:

Direct cost bookkeeping from the paper's chunk-swap lemma and elementary-streams lemma. It counts O(d) adjacent address-field interchanges per axis, in the style of standard Turing-machine transposition and data-rearrangement accounting (as in Harvey–van der Hoeven multidimensional FFT arguments).

Uses

lemSwapping binary address chunks in O(Vu^τ)lemElementary digit scans run in linear time

Used by

Nothing in the paper

Sources

PaperOpen

Section: §8.2 Growing dimension and the padded array
Page: —
Label: —
Line: sections/07-resampling.tex:380

Leannot aligned

Phase 2 aligns this node to a Lean declaration.