IterationLemma

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Iteration lemma, Step 3: crossing bad scales

ABK26, §4.3, l.iteration.lemma, Step 3. The source concatenates the good-run bound e.E.and.grad.bound.good across the maximal good intervals of ([n,m] ∩ ℤ) ∖ B, paying one factor per bad scale, and reaches e.combined.bound; two endpoint comparisons then convert it into conclusion (i), e.iteration.slope.lemma.

Both steps are proved here for abstract nonnegative sequences:

• assembleRuns --- the run concatenation, over an abstract nonnegative q;
• combinedBound --- e.combined.bound at q = E + p;
• iterationSlopeBound --- conclusion (i) in the oscillation form, from combinedBound plus the two endpoint comparisons supplied as an interface.

The prefactor: the product form, and how it differs from the printed one

The source prints the prefactor of both e.combined.bound and e.iteration.slope.lemma additively, as exp(C h + C|B| + C∑ε). What the downward induction actually yields is the product form

(goodConst h κ Cstab · badConst κ Cstab) ^ (3|B ∩ [n,m]| + 3) · exp(goodRate · ∑ε),

and since goodConst grows like h κ^h, the exponent of the product form is of order h(|B| + 1), i.e. exp(C h |B|), not exp(C(h + |B|)). The two shapes agree at the fixed h the lemma is used with (§4.4 pins h := k ≥ 3).

This module therefore proves the product form and does not claim the printed additive form. Deriving the additive form would need an argument that pays the h-cost once rather than once per good run --- conceivable, because the factor iterM h κ multiplies E_b only while p_b passes with coefficient 1, so an induction keeping the E- and p-components separate can hope to hoist it --- but it is not attempted here.

Reading choices, as implemented

• The window cap. The window nesting/sandwich is demanded only for j ≤ m. The abstract hypotheses hmono/hstab are stated for all k, which is stronger than the argument needs and is the honest shape for abstract sequences; a consumer must honour the j ≤ m cap, and no statement in this module reads E, p at any index > m: the conclusions and all sums range over [n,m], the decay hypothesis over ([n,m] ∩ ℤ) ∖ B, and the lowest index reached is n − h.
• The sandwich is not instantiated here. κ and Cstab are parameters, and AffineExcess.lean's normalizer comparison is stated at the printed aspect ratio 3^{-2}, never at the sharper 1/2.
• h and θ are data, not constants. They are explicit binders and appear in the conclusion through iterM h κ and through the gate θ^h < 3/5; no declaration hides them in an existential, and no constant here is existential.
• C is quantified outermost, depending on d alone. Implemented literally: goodConst, goodRate, badConst are explicit defs of h, κ, Cstab only, so a consumer supplying κ = κ(d), Cstab = Cstab(d) from the window geometry gets a constant uniform in n, m, B, ε, δ, u.
• The family is used on [n−h,m] while the sums range over [n,m]. Implemented literally above.
• θ^{−C(h+|B|)} versus exp(C(h+|B|)). The two shapes are reconciled only through an undisplayed relation between C and log(1/θ).
• The h-gap is never weakened. The h-gap and the gate θ^h < 3/5 are never replaced by an adjacent-scale contraction anywhere below.

Scope

hmono, hstab, hlo, hhi are hypotheses on abstract sequences here, and are the source's own Step-1/Step-3 conclusions; a consumer presenting these theorems as l.iteration.lemma itself would be turning three proof obligations into binders.

References

• ABK26, l.iteration.lemma: statement, Step 3.

Arithmetic helpers

The run concatenation

e.combined.bound and conclusion (i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.combinedBound {E p ε δ : ℤ → ℝ} {θ κ Cstab : ℝ} {h : ℕ} (hθpos : 0 < θ) (hθh : θ ^ h < 3 / 5) (hE : ∀ (k : ℤ), 0 ≤ E k) (hp : ∀ (k : ℤ), 0 ≤ p k) (hε : ∀ (k : ℤ), 0 ≤ ε k) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hκ : 1 ≤ κ) (hC : 0 ≤ Cstab) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) (hstab : ∀ (k : ℤ), |p k - p (k - 1)| ≤ Cstab * (E k + E (k - 1))) {n m : ℤ} (B : Finset ℤ) (hdecay : ∀ (j : ℤ), n ≤ j → j ≤ m → j ∉ B → E (j - ↑h) ≤ θ ^ h * E j + ε j * p j + δ j) (k : ℤ) : n ≤ k → k ≤ m → E k + p k ≤ (goodConst h κ Cstab * badConst κ Cstab) ^ (3 * (B ∩ Finset.Icc k m).card + 3) * Real.exp (goodRate Cstab * ∑ j ∈ Finset.Icc k m, ε j) * (E m + p m + ∑ j ∈ Finset.Icc k m, δ j)

e.combined.bound, in the product-prefactor form the downward induction yields (see the module docstring for the/ divergence from the printed additive form).

For every k ∈ [n,m], E_k + p_k ≤ (goodConst · badConst)^(3|B ∩ [k,m]| + 3) · exp(goodRate ∑_{[k,m]} ε) · (E_m + p_m + ∑_{[k,m]} δ), uniformly in the length m − n.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.iterationSlopeBound {E p ε δ : ℤ → ℝ} {θ κ Cstab : ℝ} {h : ℕ} (hθpos : 0 < θ) (hθh : θ ^ h < 3 / 5) (hE : ∀ (k : ℤ), 0 ≤ E k) (hp : ∀ (k : ℤ), 0 ≤ p k) (hε : ∀ (k : ℤ), 0 ≤ ε k) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hκ : 1 ≤ κ) (hC : 0 ≤ Cstab) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) (hstab : ∀ (k : ℤ), |p k - p (k - 1)| ≤ Cstab * (E k + E (k - 1))) {n m : ℤ} (hnm : n ≤ m) (B : Finset ℤ) (hdecay : ∀ (j : ℤ), n ≤ j → j ≤ m → j ∉ B → E (j - ↑h) ≤ θ ^ h * E j + ε j * p j + δ j) (osc : ℤ → ℝ) {Ci : ℝ} (hCi : 1 ≤ Ci) (hlo : osc n ≤ Ci * (E n + p n)) (hhi : E m + p m ≤ Ci * osc m) : osc n ≤ Ci ^ 2 * (goodConst h κ Cstab * badConst κ Cstab) ^ (3 * (B ∩ Finset.Icc n m).card + 3) * Real.exp (goodRate Cstab * ∑ j ∈ Finset.Icc n m, ε j) * (osc m + ∑ j ∈ Finset.Icc n m, δ j)

Conclusion (i) of l.iteration.lemma (e.iteration.slope.lemma), in the oscillation form and with the product prefactor.

The two endpoint comparisons --- which per the binding need opposite halves of the affine window geometry and are not bare triangle inequalities --- enter as the interface hypotheses hlo, hhi; they are the source's own Step-3 conclusions and must be discharged from the window sandwich at each use site, never lifted as binders into a source-facing statement.