claimroutineinferred_dep

Chirp transform and source transform procedures

Chirp transform approximates

QF_t x

; source transform approximates

RF_s

computed transforms used by the multiplication algorithm

Claim·§9.5 Chirp and source-transform procedures·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

For every disk-grid target tensor

x

with

\|x\|_\infty\le .6

, the arrays

x_0=Q_p(\overline{\widetilde a}\mathbin{\cdot}x)

satisfy

\|x_0\|_\infty\le .6

, so the computed convolution

\widetilde{\mathcal M}_{\mathbb C}

applies, and the computed chirp transform

\widetilde{\mathscr C}

returns a disk-grid array approximating

\overline a\mathbin{\cdot}\mathcal M_{\mathbb C}(a,\overline a\mathbin{\cdot}x)=QF_{\boldsymbol t}x

. Chirp construction costs

O(Tdp^{1+\delta})

in total, with

\|\widetilde a-a\|_\infty<2\,2^{-p}

. For a source disk-grid tensor of norm at most

.5

, the procedure

\widetilde{\mathscr F}

(linewise approximation to

\mathcal A

, then

\widetilde{\mathscr C}

, then linewise approximation to

\mathcal B_0

, then exact multiplication of the grid numerators by

2^\gamma

) has exact counterpart

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

, returns disk-grid outputs in

w_{\rm c}

-bit components after an exact normalization scan costing

O(Tp)

, and the opposite-sign procedure

\widetilde{\mathscr F}^{+}(z)=\overline{\widetilde{\mathscr F}(\overline z)}

has exact counterpart

RF_{\boldsymbol s}^{+}

In plain English

On disk-grid inputs of sup norm at most .6, the computed chirp transform

\widetilde{\mathscr C}

approximates

QF_{\boldsymbol t}x

, with chirp construction costing

O(Tdp^{1+\delta})

and error

\|\widetilde a-a\|_\infty<2\,2^{-p}

. The source procedure

\widetilde{\mathscr F}

(for source tensors of norm at most .5) has exact counterpart

RF_{\boldsymbol s}

, returns disk-grid outputs after an

O(Tp)

normalization scan, and its opposite-sign version

\widetilde{\mathscr F}^{+}

has exact counterpart

RF_{\boldsymbol s}^{+}

Why it's here

This turns the chirp identity into an actual computed procedure: chirp-multiply, then the computed complex convolution, then chirp-multiply, with the input norm bound ensuring the convolution black box applies. Wrapping it with the linewise resampling maps gives a computable version of

RF_{\boldsymbol s}

and, by conjugation, of

RF_{\boldsymbol s}^+

, which the multiplication algorithm and the later error-propagation and margin arguments use.

Classified routine:

Assembles Bluestein's chirp transform (chirp multiply, convolve, chirp multiply) with the earlier chirp identity, the tensor resampling lemma and the computed complex convolution. The work is bookkeeping on norms, errors and costs, following the Harvey–van der Hoeven n log n framework.

Uses

claimComplex convolution via coefficient twistlemChirp identity and source permutation cancellationlemTensor resampling across d dimensions

Used by

claimTwo scalings by S undo normalizationsclaimDisk margins and error propagation through transforms

Sources

PaperOpen

Section: §9.5 Chirp and source-transform procedures
Page: —
Label: —
Line: sections/08-assembly.tex:427

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Chirp and source-transform procedures" rests on claim-thm-main-5
info
inferred_dep
outline: "Chirp and source-transform procedures" rests on lem:chirp-permutation
info
inferred_dep
outline: "Chirp and source-transform procedures" rests on lem:tensor-resampling