claimroutine

Rows expand around exact periods

Expands each row exactly as scalar multiples of entire-function rows about periods

exact identity the later estimates bound

Claim·§3.2 Translation to entire functions·inside lemRows reduce to entire-function rows

Statement (paper)

Put

\epsilon_i=j(r_i-\omega)

and

\tau_i(t)=G_i(t)-\log(1+t)

. Since

e^{j\omega}=1

, the substitutions in read

Y=e^z

X_i=z+u_i+\epsilon_i+\tau_i(t)

with

z=j\omega+\log(1+t)

, and expanding first in the variables

u_i

, then in the constants

\epsilon_i

and tails

\tau_i

, gives the exact row vector identity for

\text{row}_{j,s,\beta}

, in which all scalar factors are independent of the column

P

In plain English

With

\epsilon_i=j(r_i-\omega)

and

\tau_i(t)=G_i(t)-\log(1+t)

, each row

\text{row}_{j,s,\beta}

equals an exact sum of scalar multiples of vectors

([t^\ell]f_{a,P}(j\omega+\log(1+t)))_P

, with all scalar factors independent of the column

P

Why it's here

Because

e^{j\omega}=1

, the row's substitution becomes

Y=e^z

and

X_i=z+u_i+\epsilon_i+\tau_i(t)

with

z=j\omega+\log(1+t)

. Expanding in the

u_i

, then the small constants

\epsilon_i

and tails

\tau_i

, writes the row as combinations of entire-function rows, which is the exact identity that the later claims bound for term weight, coefficient size and number of terms.

Classified routine:

This is a paper-specific row identity obtained by substituting

e^{j\omega}=1

and applying multivariate Taylor expansion and coefficient extraction. The argument is standard algebraic bookkeeping.

Uses

Nothing else in the paper

Used by

claimTruncation tails consume limited weightclaimCoefficient bound and term count

Sources

PaperOpen

Section: §3.2 Translation to entire functions
Page: —
Label: —
Line: sections/determinant.tex:196

Leannot aligned

Phase 2 aligns this node to a Lean declaration.