claimroutineinferred_dep

Exact normalization identity via retained order

Pointwise product commutes with layout, giving Mr\mathcal M_r exactly
exact identity the error analysis compares against
Claim·§7.1 The normalized convolution interface·inside propSynthetic convolution: error, cost, and format

Statement (paper)

Let P(u,v)P(u,v) denote the exact pointwise product uv/ruv/r and T+=Ft+B−1L−1\mathcal T_+=F_{\boldsymbol t}^+B^{-1}L^{-1}. Then P(LBu,LBv)=LBP(u,v)P(LBu,LBv)=LBP(u,v), so T+\mathcal T_+ applied to the pointwise product of the exact stored forward outputs of ff and gg equals Ft+P(Ft−f,Ft−g)F_{\boldsymbol t}^+P(F_{\boldsymbol t}^-f,F_{\boldsymbol t}^-g), and its exact scaling by MM equals Mr(f,g)\mathcal M_r(f,g), since Ft−(f∗g)=M(Ft−f)(Ft−g)F_{\boldsymbol t}^-(f*g)=M(F_{\boldsymbol t}^-f)(F_{\boldsymbol t}^-g) and Ft+Ft−=I/MF_{\boldsymbol t}^+F_{\boldsymbol t}^-=I/M give MFt+P(Ft−f,Ft−g)=(f∗g)/(rM)MF_{\boldsymbol t}^+P(F_{\boldsymbol t}^-f,F_{\boldsymbol t}^-g)=(f*g)/(rM).

In plain English

The pointwise product P(u,v)=uv/rP(u,v)=uv/r commutes with the layout and normalization maps, P(LBu,LBv)=LBP(u,v)P(LBu,LBv)=LBP(u,v). Hence applying T+=Ft+B−1L−1\mathcal T_+=F_{\boldsymbol t}^+B^{-1}L^{-1} to the pointwise product of the exact stored forward outputs of ff and gg gives Ft+P(Ft−f,Ft−g)F_{\boldsymbol t}^+P(F_{\boldsymbol t}^-f,F_{\boldsymbol t}^-g), and scaling that by MM exactly gives Mr(f,g)\mathcal M_r(f,g).

Why it's here

This is the exact, rounding-free identity behind the convolution: the layout permutation LL and normalization BB can be left in place between the forward and opposite transforms, because the pointwise product passes through them. The convolution identity Ft−(f∗g)=M(Ft−f)(Ft−g)F_{\boldsymbol t}^-(f*g)=M(F_{\boldsymbol t}^-f)(F_{\boldsymbol t}^-g) together with Ft+Ft−=I/MF_{\boldsymbol t}^+F_{\boldsymbol t}^-=I/M from the characters lemma then shows the result is Mr(f,g)\mathcal M_r(f,g). The later claims then only need to bound the rounding errors of the stored computation against this exact target and check the exact scaling by MM.
Classified routine:
Direct algebraic consequence of the convolution theorem for the synthetic DFT and the inverse relation F+F−=I/MF^+F^-=I/M from the characters lemma, plus the fact that pointwise products commute with coordinate permutations and diagonal scaling.

Uses

lemExact negacyclic product with one truncationlemCost and accuracy of synthetic transformlemRoots of unity orthogonality and inverse transforms

Used by

claimError bound and disk marginclaimExact power-of-two scaling and output format

Sources

PaperOpen
Section
§7.1 The normalized convolution interface
Page
—
Label
—
Line
sections/06-transforms.tex:657
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact normalization identity via retained order" rests on lem:synthetic-transform-cost
  • info
    inferred_dep
    outline: "Exact normalization identity via retained order" rests on lem:synthetic-characters