claimroutineinferred_dep

Axis maps contract with error dp^2

Axis maps contract;

d

axes give error

<dp^2

carries 1D error and cost bounds to

d

axes

Claim·§8.2 Growing dimension and the padded array·inside lemTensor resampling across d dimensions

Statement (paper)

Each axis map, which acts independently on its valid lines and is zero on the other lines, is a contraction and has error less than

p^2

. Hence the composition of the

d

axis maps is a contraction with error less than

dp^2

. For axis

i

at most

T/t_i

lines invoke the one-dimensional algorithm, so the total time in the one-dimensional algorithms is

\sum_{i=1}^d \frac{T}{t_i}O(t_i p^{3/2+\delta}\alpha)=O(dTp^{3/2+\delta}\alpha)

In plain English

Each axis map, which applies the one-dimensional approximation on valid lines and gives zero on other lines, is a contraction with error below

p^2

. Composing the

d

axis maps gives a contraction with error below

dp^2

, and the one-dimensional algorithms take total time

O(dTp^{3/2+\delta}\alpha)

Why it's here

This turns the one-dimensional bounds of the no-sort resampling lemma into the contraction, error

dp^2

and time claims for

\mathcal A

and

\mathcal B_0

in the tensor lemma. Lines act independently, so contraction and the

p^2

error carry over from one axis to the next and the errors add up over

d

axes. For axis

i

at most

T/t_i

lines call the one-dimensional algorithm at cost

O(t_ip^{3/2+\delta}\alpha)

each, so each axis costs

O(Tp^{3/2+\delta}\alpha)

and the sum over

d

axes gives the stated total.

Classified routine:

Direct bookkeeping consequence of the one-dimensional no-sort resampling lemma. Contractions compose, errors add under composition of contractions, and the per-axis time is summed over lines and axes.

Uses

claimTensor identity and axis-by-axis implementationlemOne-dimensional resampling without sorting

Used by

Nothing in the paper

Sources

PaperOpen

Section: §8.2 Growing dimension and the padded array
Page: —
Label: —
Line: sections/07-resampling.tex:362

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Axis maps contract; error dp^2 and line cost" rests on claim-lem-tensor-resampling-1
info
inferred_dep
outline: "Axis maps contract; error dp^2 and line cost" rests on lem:no-sort-resampling