claimroutineinferred_dep

Error bound and disk margin

Error is at most 3δ+η3\delta+\eta before scaling, keeping a disk margin
adds up transform and product rounding errors
Claim·§7.1 The normalized convolution interface·inside propSynthetic convolution: error, cost, and format

Statement (paper)

Let δ=2ℓ 2−p\delta=\sqrt2\ell\,2^{-p} and η=2 2−p\eta=\sqrt2\,2^{-p}. Then the returned opposite output h~\widetilde h satisfies ∥h~−T+P(u,v)∥∞<3δ+η\|\widetilde h-\mathcal T_+P(u,v)\|_\infty<3\delta+\eta, so after the exact multiplication by MM the approximation of Mr\mathcal M_r has error less than M(3δ+η)=2 M(3ℓ+1)2−pM(3\delta+\eta)=\sqrt2\,M(3\ell+1)2^{-p}. If one original operand has norm at most ρ<1\rho<1 and this bound is at most 1−ρ1-\rho, then ∥Mr(f,g)∥∞≤ρ\|\mathcal M_r(f,g)\|_\infty\leq\rho and the returned norm is less than ρ+(1−ρ)=1\rho+(1-\rho)=1, so the returned grid array is a disk array.

In plain English

The approximate opposite output h~\widetilde h is within 3δ+η3\delta+\eta of T+P(u,v)\mathcal T_+P(u,v) in sup norm, where δ=2ℓ2−p\delta=\sqrt2\ell 2^{-p} and η=22−p\eta=\sqrt2 2^{-p}. After exact scaling by MM this gives error less than 2M(3ℓ+1)2−p\sqrt2 M(3\ell+1)2^{-p} for Mr\mathcal M_r. If one operand has norm at most ρ<1\rho<1 and this bound is at most 1−ρ1-\rho, the returned array is a disk array.

Why it's here

This adds up the rounding errors: two forward transforms and one opposite transform each contribute δ\delta from the transform-cost lemma, and the pointwise ring product contributes η\eta from the signed ring product lemma. The exact identity from the previous claim shows the target is Mr(f,g)\mathcal M_r(f,g), so the sum bounds the total error. Since ∥Mr(f,g)∥∞≤ρ\|\mathcal M_r(f,g)\|_\infty\le\rho and the error is at most 1−ρ1-\rho, the returned norm stays below 1, which gives the disk-array conclusion of the proposition.
Classified routine:
This is standard error bookkeeping. It adds the per-transform rounding errors from the transform-cost lemma and the one-truncation error from the signed ring product lemma, then uses the exact identity from the previous claim and the triangle inequality, as in Harvey–van der Hoeven style error analysis.

Uses

lemExact negacyclic product with one truncationclaimExact normalization identity via retained orderlemCost and accuracy of synthetic transform

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Error bound √2M(3ℓ+1)2^{-p} and disk margin" rests on claim-prop-synthetic-convolution-1
  • info
    inferred_dep
    outline: "Error bound √2M(3ℓ+1)2^{-p} and disk margin" rests on lem:synthetic-transform-cost