claimroutineinferred_dep

Factorial decay of iteration differences

Gap E∗−EkE_*-E_k is at most fe1/θ1(LQ/θ1)k/k!fe^{1/\theta_1}(L_Q/\theta_1)^k/k!
quantitative convergence step fixing k∗k_*
Claim·§4.1 Correction with a fixed column multiplier·inside lemFixed point with factorial convergence

Statement (paper)

Let Δi=E∗−Ei\Delta_i=E_*-E_i. Then Δi≥0\Delta_i\geq0, the row-xx support of Δi\Delta_i is contained in AxA_x, and for every k≥0k\geq0 and all x,yx,y, Δk(x,y)≤fe1/θ1LQkfk(mxk)≤fe1/θ1(LQ/θ1)kk!\Delta_k(x,y)\leq fe^{1/\theta_1}L_Q^kf^k\binom{m_x}{k}\leq fe^{1/\theta_1}\frac{(L_Q/\theta_1)^k}{k!}, which gives max⁡x,y(E∗(x,y)−Ek(x,y))/f≤e1/θ1(LQ/θ1)k/k!\max_{x,y}(E_*(x,y)-E_k(x,y))/f\leq e^{1/\theta_1}(L_Q/\theta_1)^k/k!, so k∗k_* can be chosen as a fixed integer making this at most q−1/32q^{-1}/32.

In plain English

The gap Δi=E∗−Ei\Delta_i=E_*-E_i is nonnegative and supported within the row supports AxA_x. It satisfies Δk(x,y)≤fe1/θ1(LQ/θ1)k/k!\Delta_k(x,y)\leq fe^{1/\theta_1}(L_Q/\theta_1)^k/k!, so max⁡(E∗−Ek)/f≤e1/θ1(LQ/θ1)k/k!\max(E_*-E_k)/f\leq e^{1/\theta_1}(L_Q/\theta_1)^k/k!, and a fixed k∗k_* brings this below q−1/32q^{-1}/32.

Why it's here

This is the quantitative convergence step of the parent lemma. It starts from the entry bound E∗≤fe1/θ1E_*\leq fe^{1/\theta_1} and uses the row-support size mx≤1/(θ1f)m_x\leq 1/(\theta_1 f) to get a factor LQfL_Q f per iteration with a binomial count (mxk)≤(1/(θ1f))k/k!\binom{m_x}{k}\leq (1/(\theta_1 f))^k/k!, giving factorial decay. Since the decay is factorial and uniform in C,f,V,gC,f,V,g, a single fixed k∗k_* suffices.
Classified routine:
A direct quantitative consequence of the earlier entry bound and row-support claims. It uses the standard iteration-error estimate for a monotone fixed-point iteration together with the binomial bound (mk)≤mk/k!\binom{m}{k}\leq m^k/k!, which gives factorial decay.

Uses

claimResidual nonnegative with bounded row supportclaimEntry bound via increasing support sequences

Used by

Nothing in the paper

Sources

PaperOpen
Section
§4.1 Correction with a fixed column multiplier
Page
—
Label
—
Line
sections/hierarchy.tex:151
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Factorial decay of iteration differences" rests on claim-lem-hier-fixed-point-2
  • info
    inferred_dep
    outline: "Factorial decay of iteration differences" rests on claim-lem-hier-fixed-point-3