claimroutineinferred_dep

Tensor identity and axis-by-axis implementation

Tensoring gives the 2γ2^\gamma factor identity, implemented one axis at a time
multidimensional identity from the 1D lemma
Claim·§8.2 Growing dimension and the padded array·inside lemTensor resampling across d dimensions

Statement (paper)

Tensoring gives RFs=2γB0QFtARF_{\boldsymbol s}=2^\gamma\mathcal B_0QF_{\boldsymbol t}\mathcal A. Moreover, A\mathcal A (expansion) can be implemented by padding the input with zeros outside ∏i[0,si)\prod_i[0,s_i) and then expanding the axes one at a time, applying A~i\widetilde A_i to each line with valid other coordinates and writing tit_i zeros on every other line. Likewise B0\mathcal B_0 (compression) can be implemented axis by axis in the full box of TT entries, applying B~0,i\widetilde B_{0,i} to each tit_i-line whose other coordinates are valid and writing its sis_i outputs followed by ti−sit_i-s_i zeros, while every other line is zero and is replaced by a zero line without calling B~0,i\widetilde B_{0,i}.

In plain English

Tensoring the one-dimensional factorization gives RFs=2γB0QFtARF_{\boldsymbol s}=2^\gamma\mathcal B_0QF_{\boldsymbol t}\mathcal A. The expansion A\mathcal A and compression B0\mathcal B_0 can be implemented one axis at a time, applying A~i\widetilde A_i or B~0,i\widetilde B_{0,i} only to valid lines and filling the other lines with zeros.

Why it's here

This gives the multidimensional identity from the one-dimensional lemma, since the factors 22α22^{2\alpha^2} multiply to 22dα2=2γ2^{2d\alpha^2}=2^\gamma. It also describes the padded-box, line-by-line procedure whose contraction, error and cost properties are analysed in the following claims. Valid lines get the one-dimensional approximation, and the remaining lines are zero and skip it, which keeps the work proportional to the valid lines.
Classified routine:
Direct tensoring of the one-dimensional factorization from lem-no-sort-resampling, implemented with the standard axis-by-axis (row-column) technique for applying tensor-product operators to multidimensional arrays, as in Harvey–van der Hoeven's Gaussian resampling.

Uses

lemOne-dimensional resampling without sorting

Used by

claimAxis maps contract with error dp^2

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Tensor identity and linewise expansion/compression" rests on lem:no-sort-resampling