claimroutineinferred_dep

Coefficient bound and term count

Bounds each scalar by

\exp\{-\nu w(a-\beta)+HE_{\rm tr}\}

and counts ≤

Q_H

terms

explicit estimates finishing the translation lemma

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

Statement (paper)

Every nonzero scalar

\xi

occurring with index

a

in satisfies

\log|\xi|\le -\nu w(a-\beta)+\frac{\nu H}{F_0}+\frac{H\log 2}{v_0}+\frac{H(\log4+\log(2K)+\nu)}{w_*}

, that is,

|\xi|\le\exp\{-\nu w(a-\beta)+HE_{\rm tr}\}

(and the bound holds trivially for a zero scalar). Moreover each coordinate of

a

and

d

is at most

H

and

0\le k\le H/v_0

, so the number of terms is at most

Q_H=(\lfloor H\rfloor+1)^{2m}(\lfloor H/v_0\rfloor+1)

In plain English

Every scalar

\xi

attached to an index

a

in the row identity satisfies

|\xi|\le\exp\{-\nu w(a-\beta)+HE_{\rm tr}\}

, where

E_{\rm tr}

collects the

\nu H/F_0

H\log 2/v_0

and

H(\log4+\log(2K)+\nu)/w_*

contributions. Also, the coordinates of

a

and

d

are at most

H

and

0\le k\le H/v_0

, so there are at most

Q_H=(\lfloor H\rfloor+1)^{2m}(\lfloor H/v_0\rfloor+1)

terms.

Why it's here

This finishes the proof of the translation lemma by turning the exact row identity into explicit estimates. The tail-weight bound from the previous claim supplies the

\nu H/F_0

part of

E_{\rm tr}

, and counting the admissible index ranges gives

Q_H

, so each row is a controlled sum of entire-function rows.

Classified routine:

This is bookkeeping from the exact row expansion in claim-det-translation-1 and the tail-weight estimate in claim-det-translation-2: bound the coefficients, collect their contributions into

E_{\rm tr}

, and count the allowed index ranges.

Uses

claimRows expand around exact periodsclaimTruncation tails consume limited weight

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Approximation errors control coefficients and count" rests on claim-det-translation-1
info
inferred_dep
outline: "Approximation errors control coefficients and count" rests on claim-det-translation-2