lemmaroutineunresolved_ref

One-dimensional resampling without sorting

Writes PsFs=22α2B0PtFtAP_sF_s=2^{2\alpha^2}B_0P_tF_tA with cheap ordered contractions
one-dimensional step reaching prime lengths from tit_i
Lemma·lem:no-sort-resampling·§8.1 The one-dimensional interface

Statement (paper)

Fix 0<δ<1/80<\delta<1/8. Let p>100p>100, 2≤s<t<2p2\leq s<t<2^p and 2≤α<p2\leq\alpha<\sqrt p be integers, with gcd⁡(s,t)=1\gcd(s,t)=1 and θ:=t/s−1>p/α4. \theta:=t/s-1>p/\alpha^4. Define coordinate permutations by (Psu)j=utj,(Ptv)k=v−sk. (P_su)_j=u_{tj},\qquad (P_tv)_k=v_{-sk}. There are linear contractions A:Cs→CtA:\mathbb C^s\to\mathbb C^t and B0:Ct→CsB_0:\mathbb C^t\to\mathbb C^s satisfying PsFs=22α2B0PtFtA. P_sF_s=2^{2\alpha^2}B_0P_tF_tA. There are fixed multitape algorithms for approximations A~:Dps→Dpt\widetilde A:\mathbb D_p^s\to\mathbb D_p^t and B~0:Dpt→Dps\widetilde B_0:\mathbb D_p^t\to\mathbb D_p^s, each with error less than p2p^2 and time O(tp3/2+δα). O(tp^{3/2+\delta}\alpha). The constant is uniform in p,s,t,αp,s,t,\alpha. Inputs and outputs use the scalar component format above and occur in increasing coordinate order.

In plain English

For coprime 2≤s<t<2p2\le s<t<2^p with t/s−1>p/α4t/s-1>p/\alpha^4 and 2≤α<p2\le\alpha<\sqrt p, the permuted length-ss transform factors as PsFs=22α2B0PtFtAP_sF_s=2^{2\alpha^2}B_0P_tF_tA through the permuted length-tt transform, with linear contractions AA and B0B_0. Both AA and B0B_0 have fixed multitape approximations on Dp\mathbb D_p with error below p2p^2 and time O(tp3/2+δα)O(tp^{3/2+\delta}\alpha), reading and writing coordinates in increasing order.

Why it's here

This is the one-dimensional interface that lets a length-ss transform be computed from a length-tt transform, with the coordinate permutations left in place so no sorting is needed. The proof builds an exact factorization from a resampling map, a Neumann-series inverse and a diagonal scaling, then bounds the errors and costs of the ordered numerical versions. The tensor-resampling lemma uses it axis by axis, and the main theorem uses it to reach the chosen prime lengths sis_i from tit_i.
Classified routine:
This adapts the Gaussian resampling theorem of Harvey–van der Hoeven (Integer multiplication in time O(n log n)), which factors a length-s DFT through a length-t DFT using a resampling map, a Neumann-series inverse and a diagonal scaling. The change here is that the coordinate permutations are left in place, so no sorting step is needed on the Turing machine.

Uses

Nothing else in the paper

Used by

lemTensor resampling across d dimensionsclaimTensor identity and axis-by-axis implementationclaimAxis maps contract with error dp^2claimDistinct primes meet resampling hypotheses

Inside the proof

claimExact resampling identity with permutations retainedclaimOrdered approximations with error and time boundsclaimRecord format conversions are cheap and exactclaimTape movement and Neumann iteration bounds

Sources

PaperOpen
Section
§8.1 The one-dimensional interface
Page
—
Label
lem:no-sort-resampling
Line
sections/07-resampling.tex:53
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    The exact Gaussian identity, inverse estimate, contraction bounds and numerical maps are imported from Harvey–van der Hoeven (Theorem 4.2, Lemma 4.6, Prop. 4.7, Lemmas 4.8–4.12).