IterationGoodRun

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

Iteration lemma, Step 2 on a run of good scales

ABK26, §4.3, l.iteration.lemma, Step 2. Given the reabsorption of IterationCore.lean, the source runs the discrete Grönwall lemma on a_l:= |∇ℓ_{b−l} − ∇ℓ_b| to obtain e.grad.bound.good, substitutes back into e.sum.excess.bound to get the same bound for E_i, and arrives at e.E.and.grad.bound.good. This module proves that chain for abstract nonnegative sequences:

• slopeGronwall --- e.grad.bound.good: the pointwise slope bound on the run, obtained from reabsorbSum + slopeTelescope + discrete_gronwall;
• goodRunBound --- e.E.and.grad.bound.good at the bottom of the run: E_a + p_a ≤ goodConst · (E_b + p_b + ∑δ) · exp(goodRate · ∑ε), with no dependence on the run length.

Source gaps this module has to fill (disclosed, from the graph NOTEs)

• does not write the reindexing a_l := |∇ℓ_{b−l} − ∇ℓ_b|, nor the identification of Grönwall's H, nor the final passage from a bound on |∇ℓ_i − ∇ℓ_b| to one on |∇ℓ_i|. All three are performed explicitly here; H is 5 Cstab (iterM · E_b + p_b ∑ε + ∑δ).
• performs the split |∇ℓ_k| ≤ |∇ℓ_b| + |∇ℓ_k − ∇ℓ_b| silently; it is the step hεp below, and it is what makes the Grönwall recursion linear in the unknown |∇ℓ_k − ∇ℓ_b|.
• asserts "Substituting back into e.sum.excess.bound gives the same bound for E_i"; the substitution produces a sum ∑ ε_k |∇ℓ_k| each of whose summands carries its own exponential, and the collapse to a single exponential is not shown. Here the collapse is explicit: every summand is bounded by the uniform run bound before summation, which is why slopeGronwall is proved for all k in the run and not only at the bottom.
• the δ-sum index silently shifts between; the shape proved here uses the full run sum ∑_{[a,b]} δ in both places, which dominates either printed range.

Constants

The θ^h < 3/5 gate enters only through reabsorbSum; h enters only through iterM. Real.exp is kept opaque: the only facts used are x ≤ exp x, monotonicity, and exp(x)exp(y) = exp(x+y).

Scope

hmono/hstab are binders on the abstract sequences here and are not hypotheses of the source lemma (see IterationCore.lean); nothing in this module may be presented as l.iteration.lemma or as any part of it closed.

References

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

The slope bound on a run (e.grad.bound.good)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.slopeGronwall {E p ε δ : ℤ → ℝ} {Cstab M : ℝ} {h : ℕ} (hC : 0 ≤ Cstab) (hM : 0 ≤ M) (hE : ∀ (k : ℤ), 0 ≤ E k) (hp : ∀ (k : ℤ), 0 ≤ p k) (hε : ∀ (k : ℤ), 0 ≤ ε k) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hstab : ∀ (k : ℤ), |p k - p (k - 1)| ≤ Cstab * (E k + E (k - 1))) (hh : 1 ≤ h) {a b : ℤ} (hab : a ≤ b) (hUb : ∀ (i : ℤ), a ≤ i → i ≤ b → ∑ k ∈ Finset.Icc i b, E k ≤ 5 / 2 * (M * E b + ∑ k ∈ Finset.Icc (i + ↑h) b, (ε k * p k + δ k))) (k : ℤ) : a ≤ k → k ≤ b → |p k - p b| ≤ 5 * Cstab * (M * E b + p b * ∑ j ∈ Finset.Icc a b, ε j + ∑ j ∈ Finset.Icc a b, δ j) * Real.exp (5 * Cstab * ∑ j ∈ Finset.Icc a b, ε j)

e.grad.bound.good, uniform on the run [a,b].

The hypothesis hUb is the reabsorption e.sum.excess.bound at every base point of the run; the conclusion is the Grönwall output at every point of the run.

The fold into the good-run constant

The good-run bound (e.E.and.grad.bound.good)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.goodRunBound {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))) {a b : ℤ} (hab : a ≤ b) (hdecay : ∀ (j : ℤ), a ≤ j → j ≤ b → E (j - ↑h) ≤ θ ^ h * E j + ε j * p j + δ j) : E a + p a ≤ goodConst h κ Cstab * (E b + p b + ∑ k ∈ Finset.Icc a b, δ k) * Real.exp (goodRate Cstab * ∑ k ∈ Finset.Icc a b, ε k)

e.E.and.grad.bound.good at the bottom of a run of good scales, in the length-independent form the assembly consumes:

E_a + p_a ≤ goodConst h κ Cstab · (E_b + p_b + ∑_{[a,b]} δ) · exp(goodRate Cstab · ∑_{[a,b]} ε).

1 ≤ h is not assumed: it follows from θ^h < 3/5.