claimroutineinferred_dep

Entry bound via increasing support sequences

Entries satisfy

E_*(x,y)\le fe^{1/\theta_1}

starting estimate for the factorial decay

Claim·§4.1 Correction with a fixed column multiplier·inside lemFixed point with factorial convergence

Statement (paper)

For every

x,y

E_*(x,y)\leq f\sum_{j=0}^{m_x}\binom{m_x}{j}f^j=f(1+f)^{m_x}\leq fe^{1/\theta_1}

, where

m_x=|A_x|

is the cardinality of

A_x=\{y:E_*(x,y)>0\}

and

m_x\leq 1/(\theta_1 f)

In plain English

Every entry of the fixed-point solution satisfies

E_*(x,y)\leq f(1+f)^{m_x}\leq fe^{1/\theta_1}

, where

m_x=|A_x|

is the size of the support of row

x

and

m_x\leq 1/(\theta_1 f)

Why it's here

This turns the row-support bound

m_x\leq 1/(\theta_1 f)

from the previous claim into a uniform entrywise bound:

(1+f)^{m_x}\leq e^{f m_x}\leq e^{1/\theta_1}

. The factorial decay of

E_*-E_k

in the next claim uses this bound as its starting estimate, and the binomial sum in the statement is the count of subsets of the row support that this estimate runs over.

Classified routine:

The bound follows from the previous claim's row-support bound

m_x\leq 1/(\theta_1 f)

by expanding over subsets of the support (a binomial sum), then applying

(1+f)^{m}\leq e^{fm}

. This is a standard counting and calculus estimate, not a new idea.

Uses

claimResidual nonnegative with bounded row support

Used by

claimFactorial decay of iteration differences

Sources

PaperOpen

Section: §4.1 Correction with a fixed column multiplier
Page: —
Label: —
Line: sections/hierarchy.tex:127

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Entry bound via increasing support sequences" rests on claim-lem-hier-fixed-point-2