claimroutineinferred_dep

Total cost of transforms and products

Total cost

O(Tp[dK+pK^{\tau-1}+\ell d^{\lambda'}+\log(rp)])

sums transform and pointwise product costs

Claim·§7.1 The normalized convolution interface·inside propSynthetic convolution: error, cost, and format

Statement (paper)

The

M=T/r

pointwise polynomial products have total cost

O(Tp\log(rp))

. Together with the three transform costs as stated in Lemma , the linear-in-

Tp

exact scaling, and the data movement by the previously specified scans, swaps, and layout restoration, the total cost is

O\left(Tp\left[dK+pK^{\tau-1}+\ell d^{\lambda'}+\log(rp)\right]\right)

In plain English

The

M=T/r

pointwise polynomial products cost

O(Tp\log(rp))

in total. Adding the three transform costs, the linear-in-

Tp

exact scaling, and data movement, the whole procedure costs

O(Tp[dK+pK^{\tau-1}+\ell d^{\lambda'}+\log(rp)])

Why it's here

Each pointwise product costs

O(rp\log(rp))

by the signed ring product lemma, so

M=T/r

of them cost

O(Tp\log(rp))

, which gives the

\log(rp)

term. The two transform-lemma applications and the forward transform supply the

dK

pK^{\tau-1}

and

\ell d^{\lambda'}

terms, and the remaining scaling and scan steps are linear in

Tp

and absorbed, giving the cost bound in the proposition.

Classified routine:

Direct cost bookkeeping: it sums M=T/r applications of the signed ring product lemma (O(rp log(rp)) each) with the transform costs from Lemma lem-synthetic-transform-cost and the linear-time scans.

Uses

lemCost and accuracy of synthetic transformlemExact negacyclic product with one truncation

Used by

Nothing in the paper

Sources

PaperOpen

Section: §7.1 The normalized convolution interface
Page: —
Label: —
Line: sections/06-transforms.tex:733

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Total cost of transforms and products" rests on lem:synthetic-transform-cost
info
inferred_dep
outline: "Total cost of transforms and products" rests on lem:signed-ring-product