IterationCore

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

Iteration lemma, Step 1 and the Step-2 reabsorption

ABK26, §4.3, inside the proof of l.iteration.lemma. This module proves the three length-independent ingredients of Steps 1--2, for abstract nonnegative sequences E p ε δ : ℤ → ℝ:

• the constants iterM, goodConst, goodRate, badConst, all explicit polynomial expressions in h, κ, Cstab (no existential constants: the development's own do-not-repeat list records that existential constants make downstream uniformity unprovable in principle);
• one-scale comparability badCrossing: `E_{k-1} + p_{k-1} ≤ badConst (E_k
  • p_k), the e.combined.bound` input for crossing a bad scale;
• the reabsorption reabsorbSum (e.sum.excess.bound): on a run of good scales [a,b], ∑_{[i,b]} E is controlled by the single top value E_b (times h κ^h) plus the error sums, with no dependence on the run length. This is the estimate that stops the good-run bound from blowing up over long runs, and it is where θ^h < 3/5 is used;
• the telescoped slope stability slopeTelescope, i.e. e.grad.stability summed across a run.

Faithfulness notes on this layer (all disclosed, none resolved here)

• hmono (E_k ≤ κ E_{k+1}) and hstab (|p_k − p_{k−1}| ≤ Cstab(E_k+E_{k−1})) appear here as hypotheses on the abstract sequences. They are not hypotheses of the source lemma: the source derives them from the window sandwich (e.grad.stability, and quasi-monotonicity from nestedness). Nothing in this tree may be presented as l.iteration.lemma while hmono/hstab are binders.
• (tex-binding on the constant): the source prints the reabsorption factor 3^{(d+2)h}, which is κ^h for the per-scale quasi-monotonicity constant κ; the source's own sandwich only gives κ = 3^{1+3d/2}, and 1 + 3d/2 ≤ d+2 iff d ≤ 2, so the printed constant is too small for every d ≥ 3. This module therefore keeps κ as a parameter and never instantiates it at 3^{d+2}: the factor carried is h κ^h (iterM), honest for whatever κ the geometry supplies.
• Accordingly reabsorbSum is stated for the h-scale-gap recurrence E_{j−h} ≤ θ^h E_j + … with the numerical gate θ^h < 3/5, and never for an adjacent-scale recurrence. The h-gap and the θ^h < 3/5 gate are load-bearing, not slack.

Scope

l.iteration.lemma is an unfrozen source node; nothing here claims a node, or a fraction of one, closed.

References

• ABK26, l.iteration.lemma proof, Step 1, Step 2.

The explicit constants

def Algsuperdiff.Section4.Provider.ExcessDecay.iterM (h : ℕ) (κ : ℝ) : ℝ

The reabsorption factor of e.sum.excess.bound: h κ^h. The source prints 3^{(d+2)h} that value is too small for d ≥ 3, so κ is kept as a parameter.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.iterM h κ = ↑h * κ ^ h

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.goodConst (h : ℕ) (κ Cstab : ℝ) : ℝ

The good-run constant, as recomputed in IterationGoodRun.lean.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section4.Provider.ExcessDecay.goodRate (Cstab : ℝ) : ℝ

The exponential rate of the good-run bound: exp(goodRate · ∑ ε).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.goodRate Cstab = 5 * Cstab + 2

def Algsuperdiff.Section4.Provider.ExcessDecay.badConst (κ Cstab : ℝ) : ℝ

The one-scale crossing constant.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.badConst κ Cstab = κ + Cstab * (1 + κ)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.iterM_nonneg (h : ℕ) {κ : ℝ} (hκ : 1 ≤ κ) : 0 ≤ iterM h κ

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_goodConst (h : ℕ) {κ Cstab : ℝ} (hκ : 1 ≤ κ) (hC : 0 ≤ Cstab) : 1 ≤ goodConst h κ Cstab

theorem Algsuperdiff.Section4.Provider.ExcessDecay.goodRate_nonneg {Cstab : ℝ} (hC : 0 ≤ Cstab) : 0 ≤ goodRate Cstab

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_badConst {κ Cstab : ℝ} (hκ : 1 ≤ κ) (hC : 0 ≤ Cstab) : 1 ≤ badConst κ Cstab

One-scale comparability

theorem Algsuperdiff.Section4.Provider.ExcessDecay.badCrossing {E p : ℤ → ℝ} {κ Cstab : ℝ} (hE : ∀ (k : ℤ), 0 ≤ E k) (hκ : 1 ≤ κ) (hC : 0 ≤ Cstab) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) (hp : ∀ (k : ℤ), 0 ≤ p k) (hstab : ∀ (k : ℤ), |p k - p (k - 1)| ≤ Cstab * (E k + E (k - 1))) (k : ℤ) : E (k - 1) + p (k - 1) ≤ badConst κ Cstab * (E k + p k)

One-scale crossing: E_{k−1} + p_{k−1} ≤ badConst (E_k + p_k). The source reads this off e.grad.stability "and the definition of excess"; here it is read off the abstract hmono/hstab.

Reindexing helpers

theorem Algsuperdiff.Section4.Provider.ExcessDecay.refl_sum (F : ℤ → ℝ) (c : ℤ) (l : ℕ) : ∑ t ∈ Finset.range l, F (c - ↑t) = ∑ k ∈ Finset.Icc (c - ↑l + 1) c, F k

Reflection reindex: a range sum of a reflected function is an Icc sum.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sum_Icc_shift (f : ℤ → ℝ) (a b h : ℤ) : ∑ j ∈ Finset.Icc (a + h) b, f (j - h) = ∑ k ∈ Finset.Icc a (b - h), f k

Shift reindex: ∑_{[a+h,b]} f(j−h) = ∑_{[a,b−h]} f.

The reabsorption of the excess sum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessIterMono {E : ℤ → ℝ} {κ : ℝ} (hκ0 : 0 ≤ κ) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) (t : ℕ) (c : ℤ) : E c ≤ κ ^ t * E (c + ↑t)

Iterated quasi-monotonicity: E c ≤ κ^t E (c + t).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.topHBound {E : ℤ → ℝ} {κ : ℝ} {h : ℕ} (hκ : 1 ≤ κ) (hE : ∀ (k : ℤ), 0 ≤ E k) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) (b : ℤ) : ∑ k ∈ Finset.Icc (b - ↑h + 1) b, E k ≤ iterM h κ * E b

The top h terms of the excess sum are controlled by E_b: this is where the factor iterM h κ = h κ^h (the source's 3^{(d+2)h}) comes from.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reabsorbSum {E p ε δ : ℤ → ℝ} {θ κ : ℝ} {h : ℕ} (hθpos : 0 < θ) (hθh : θ ^ h < 3 / 5) (hE : ∀ (k : ℤ), 0 ≤ E k) (hε : ∀ (k : ℤ), 0 ≤ ε k) (hp : ∀ (k : ℤ), 0 ≤ p k) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hκ : 1 ≤ κ) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) {a b : ℤ} (hdecay : ∀ (j : ℤ), a ≤ j → j ≤ b → E (j - ↑h) ≤ θ ^ h * E j + ε j * p j + δ j) : ∑ k ∈ Finset.Icc a b, E k ≤ 5 / 2 * (iterM h κ * E b + ∑ k ∈ Finset.Icc (a + ↑h) b, (ε k * p k + δ k))

Reabsorption of the excess sum (e.sum.excess.bound).

On a run of scales [a,b] carrying the h-gap decay recurrence, the excess sum from any i ∈ [a,b] to b is controlled by E_b alone, up to the error sums, with no dependence on b − i. The numerical gate θ^h < 3/5 is what makes the reabsorption possible; the error sum starts at i + h, which is the honest range at which summing the recurrence produces error terms.

The telescoped slope stability

theorem Algsuperdiff.Section4.Provider.ExcessDecay.slopeTelescope {E p : ℤ → ℝ} {Cstab : ℝ} (hC : 0 ≤ Cstab) (hE : ∀ (k : ℤ), 0 ≤ E k) (hstab : ∀ (k : ℤ), |p k - p (k - 1)| ≤ Cstab * (E k + E (k - 1))) (b : ℤ) (l : ℕ) : |p (b - ↑l) - p b| ≤ 2 * Cstab * ∑ k ∈ Finset.Icc (b - ↑l) b, E k

Telescoped e.grad.stability (summed): the slope difference across a run is controlled by twice Cstab times the excess sum. The factor 2 is the honest accounting: each E_k occurs in at most two of the telescoped pairs.