claimroutineinferred_dep

Residual nonnegative with bounded row support

Residual

T

is nonnegative, ≥

\theta_1f

on the support, so rows have ≤

1/(\theta_1f)

entries

row-support size bound for entry and decay estimates

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

Statement (paper)

With

T=C-E_*+E_*C

, one has

T\geq0

T(x,y)\geq\theta_1f

at every position

(x,y)

where

E_*(x,y)>0

, and

T\mathbf 1\leq C\mathbf 1\leq\mathbf 1

. Consequently, for each row

x

, the support

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

has cardinality

m_x\leq 1/(\theta_1f)

In plain English

Setting

T=C-E_*+E_*C

, the matrix

T

is entrywise nonnegative, satisfies

T(x,y)\geq\theta_1 f

wherever

E_*(x,y)>0

, and has row sums at most those of

C

, so

T\mathbf 1\leq C\mathbf 1\leq\mathbf 1

. Hence each row's support

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

has size

m_x\leq 1/(\theta_1 f)

Why it's here

Where

E_*

is positive, the fixed-point equation forces

T

to be at least

\theta_1 f

, and the row-sum bound

T\mathbf 1\leq\mathbf 1

then caps how many such positions a row can have. This bound on

m_x

is what the later entry bound and the factorial decay of

E_*-E_k

rely on, building on the existence and nonnegativity of

E_*

from the previous claim.

Classified routine:

A direct consequence of the fixed-point equation from the previous claim: entrywise nonnegativity plus a row-sum (counting) bound caps the support size at 1/(θ_1 f), with no new technique involved.

Uses

claimFixed point exists uniquely by forward ordering

Used by

claimEntry bound via increasing support sequencesclaimFactorial decay of iteration differences

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Fixed-point residual nonnegative, bounded row support" rests on claim-lem-hier-fixed-point-1