lemmaroutineinferred_dep

Chirp identity and source permutation cancellation

Chirp turns QFtQF_t into a convolution; RR cancels in the product pipeline
converts transforms to convolutions and fixes normalization
Lemma·lem:chirp-permutation·§8.3 The middle transform and the final permutation

Statement (paper)

With R,Q,si,tiR,Q,s_i,t_i as in Lemma , assume every tit_i is even. For j∈Zd\boldsymbol j\in\mathbb Z^d, define aj=exp⁡(−πi∑i=1dsiji2ti). a_{\boldsymbol j} =\exp\left(-\pi i\sum_{i=1}^d\frac{s_i j_i^2}{t_i}\right). Then aa has period tit_i in coordinate ii, and QFtu=a‾⋅a∗(a‾⋅u)T. QF_{\boldsymbol t}u =\overline a\mathbin{\cdot} \frac{a*(\overline a\mathbin{\cdot}u)}{T}. If S=∏isiS=\prod_i s_i, then (RFs+)[(RFsu)⋅(RFsv)]=u∗vS2. (RF_{\boldsymbol s}^+) \bigl[(RF_{\boldsymbol s}u)\mathbin{\cdot} (RF_{\boldsymbol s}v)\bigr] =\frac{u*v}{S^2}. Complex conjugation of the input and output of an algorithm for RFsRF_{\boldsymbol s} gives an algorithm for RFs+RF_{\boldsymbol s}^+.

In plain English

When every tit_i is even, the chirp aj=exp⁡(−πi∑isiji2/ti)a_{\boldsymbol j}=\exp(-\pi i\sum_i s_i j_i^2/t_i) has period tit_i in coordinate ii, and the permuted transform satisfies QFtu=a‾⋅(a∗(a‾⋅u))/TQF_{\boldsymbol t}u=\overline a\cdot (a*(\overline a\cdot u))/T, a chirp-multiply, convolve, chirp-multiply form. Also (RFs+)[(RFsu)⋅(RFsv)]=(u∗v)/S2(RF_{\boldsymbol s}^+)[(RF_{\boldsymbol s}u)\cdot(RF_{\boldsymbol s}v)]=(u*v)/S^2 with S=∏isiS=\prod_i s_i, and conjugating the input and output of an algorithm for RFsRF_{\boldsymbol s} gives one for RFs+RF_{\boldsymbol s}^+.

Why it's here

This turns the permuted transform QFtQF_{\boldsymbol t} that appears in the tensor resampling factorization into a convolution with a chirp, so it can be computed as a convolution. It also shows that the permutation RR cancels in the pointwise-product multiplication pipeline, leaving (u∗v)/S2(u*v)/S^2, which is the normalization bookkeeping used for the final multiplication and its error analysis. The conjugation remark gives the inverse-side transform RFs+RF_{\boldsymbol s}^+ at no extra cost.
Classified routine:
A direct calculation adapting Bluestein's chirp-z identity (jk = (j^2 + k^2 - (j-k)^2)/2) to the permuted transform QF_t. The cancellation of R is the convolution theorem bookkeeping, following the Harvey–van der Hoeven n log n framework.

Uses

lemTensor resampling across d dimensions

Used by

claimChirp transform and source transform proceduresclaimTwo scalings by S undo normalizationsclaimFinal error below 1/2; rounding and carries exact

Sources

PaperOpen
Section
§8.3 The middle transform and the final permutation
Page
—
Label
lem:chirp-permutation
Line
sections/07-resampling.tex:416
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The statement at sections/07-resampling.tex:418 takes "R,Q,s_i,t_i as in Lemma ", but the DAG records no use.