lemmaroutineinferred_dep

Tensor resampling across d dimensions

Lifts resampling to

d

axes with error

dp^2

and factor

2^\gamma

multidimensional resampling used by chirp and cost table

Lemma·lem:tensor-resampling·§8.2 Growing dimension and the padded array

Statement (paper)

Suppose every pair

(s_i,t_i)

1\leq i\leq d

, satisfies Lemma with the same

p,\alpha,\delta

. Put

T=\prod_i t_i

\gamma=2d\alpha^2

, and

R=\bigotimes_iP_{s_i},\quad Q=\bigotimes_iP_{t_i},\quad \mathcal A=\bigotimes_i A_i,\quad \mathcal B_0=\bigotimes_i B_{0,i}.

Then

RF_{\boldsymbol s} =2^\gamma\mathcal B_0QF_{\boldsymbol t}\mathcal A, \qquad F_{\boldsymbol q}:=\bigotimes_iF_{q_i}.

Also write

F_{\boldsymbol q}^+=\bigotimes_iF_{q_i}^+

. Both

\mathcal A

and

\mathcal B_0

are contractions. The linewise implementations of

\mathcal A

and

\mathcal B_0

each have error less than

dp^2

. The total time spent in the one-dimensional algorithms for both maps is

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

, with a constant independent of

d

. If each

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

with

r=2^\ell

, the array is kept in the full padded box of

T

entries, and each entry occupies

O(p)

bits, then exposing and restoring all the lines costs

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

using the equal-width chunk-swap bound

O(Vu^\tau)

and the fixed-digit movement primitive. Any fixed polynomial in

p

of setup per line is negligible compared with

Tp

when

r

grows faster than every such polynomial and

d

is polynomially bounded in

p

In plain English

If each pair

(s_i,t_i)

satisfies the one-dimensional no-sort resampling lemma with common

p,\alpha,\delta

, then

RF_{\boldsymbol s}=2^\gamma\mathcal B_0QF_{\boldsymbol t}\mathcal A

with

\gamma=2d\alpha^2

, where

\mathcal A

and

\mathcal B_0

are tensor products of the one-dimensional maps. Both are contractions, their linewise implementations have error below

dp^2

and use

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

time in the one-dimensional algorithms, and when each

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

exposing and restoring all lines in the padded box costs

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

Why it's here

This lifts the one-dimensional resampling factorization to a multidimensional transform by tensoring, so a transform with lengths

s_i

can be computed from one with lengths

t_i

at controlled error and cost. The factors

2^{2\alpha^2}

multiply to

2^\gamma

, the maps act line by line so contraction and error bounds carry over axis by axis, and the data movement needed to expose each axis is bounded using the chunk-swap and elementary-stream primitives. The later chirp, prime-length and cost-table arguments rely on these identity, error and cost statements.

Classified routine:

Direct tensor-product lift of the one-dimensional no-sort resampling lemma (as in Harvey–van der Hoeven's multidimensional Gaussian resampling), with error and cost bookkeeping axis by axis using the earlier chunk-swap and elementary-stream primitives.

Uses

lemSwapping binary address chunks in O(Vu^τ)lemElementary digit scans run in linear timelemOne-dimensional resampling without sorting

Used by

lemChirp identity and source permutation cancellationclaimDistinct primes meet resampling hypothesesclaimChirp transform and source transform proceduresclaimDisk margins and error propagation through transformsclaimCost table yields the final time bound

Inside the proof

claimTensor identity and axis-by-axis implementationclaimAxis maps contract with error dp^2claimAxis exposure costs via chunk swapsclaimPer-line setup cost is negligible

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The statement at sections/07-resampling.tex:307-308 says "every pair (s_i,t_i) ... satisfies Lemma ", and the proof tensors its identity (line 342). The edge exists only on claims, not on the lemma itself.