WeightedGoodRun

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

The θ-weighted good-run iterate and the weighted run assembly

ABK26, §4.3, inside the proof of l.iteration.lemma, Step 4 and Step 3, for abstract nonnegative sequences E δ w : ℤ → ℝ.

IterationExcessDecay.goodRunExcessIterate iterates the h-gap decay recurrence and discards every θ-weight on the error terms, which is what the source's own display does. The decay-carrying half of the lemma needs the opposite bookkeeping: the weights must be kept, because the geometric series

∑_{r ≥ 0} (θ^h)^r ≤ 1/(1 − 3/5) = 5/2       (θ^h < 3/5)

then bounds the whole accumulated w-budget of a run by (5/2)·(a single bound Mp for w on the run), with no dependence on the run length. That is the only reason a single power of the error scale survives to the bottom of [n,m]; with the weights discarded one gets a length-dependent ∑_j w_j instead.

Three results, all abstract:

• weightedGoodRunIterate --- the weighted iterate. The geometric series is internalised: the induction carries the closed budget (5/2)·Mp and the step θ^h·(5/2)Mp + Mp ≤ (5/2)Mp is exactly the geometric estimate at θ^h ≤ 3/5 ((3/5)(5/2) + 1 = 5/2, an equality --- the gate is used at full strength here).
• weightedRunBound --- the same bound at the exact bottom a of a run [a,b]. The iterate only reaches b − t h; the remaining s = (b−a) mod h scales are crossed with quasi-monotonicity, and the θ-power is restored to the geometric θ^{b−a} at the cost of the division remainder (κ θ^{-1})^h.
• weightedAssemble --- the downward run assembly across B: one factor Λ = 2(κθ^{-1})^{h+2} per bad scale (plus one for the initial run), the payoff being the genuine θ^{m−k} on the top excess and a length-independent error budget.

What the θ-powers cost, and why the anchor's prefactor has room for it

Each bad scale is crossed with E_{k−1} ≤ κ E_k, which loses one power of θ against the θ^{m−k} bookkeeping, and each good run loses at most θ^{-(h+1)} (the division remainder plus the two crossings). The assembly therefore pays θ^{-(h+2)(|B ∩ [k,m]| + 1)}, which is below the frozen statement's θ^{-C(h+1)(|B|+1)} for any C ≥ 2: the θ-power prefactor of conclusion (ii) is the legitimate division remainder, and it is ≥ 1 because θ < 1, so it is slack, never a burden.

References

• ABK26, l.iteration.lemma Step 3, Step 4; conclusion (ii) e.excess.decay.lemma.

θ-power bookkeeping

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_inv_of_le_one {θ : ℝ} (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) : 1 ≤ θ⁻¹

On (0,1] the inverse is at least one; this is the only sign fact the θ-payback factors need.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_mul_inv {θ κ : ℝ} (hκ : 1 ≤ κ) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) : 1 ≤ κ * θ⁻¹

1 ≤ κ θ^{-1}: the per-scale payback factor of the assembly.

The weighted iterate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.weightedGoodRunIterate {E δ w : ℤ → ℝ} {θ Mp : ℝ} {h : ℕ} (hθpos : 0 < θ) (hθh : θ ^ h < 3 / 5) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hMp : 0 ≤ Mp) {a b : ℤ} (hwM : ∀ (j : ℤ), a ≤ j → j ≤ b → w j ≤ Mp) (hdecay : ∀ (j : ℤ), a ≤ j → j ≤ b → E (j - ↑h) ≤ θ ^ h * E j + w j + δ j) (t : ℕ) : a ≤ b - ↑t * ↑h → E (b - ↑t * ↑h) ≤ (θ ^ h) ^ t * E b + 5 / 2 * Mp + ∑ j ∈ Finset.Icc (b - ↑t * ↑h + 1) b, δ j

The θ-weighted good-run iterate (first display, with the weights kept).

On a run [a,b] carrying the h-gap decay recurrence, with the error scale w bounded by Mp on the run,

E_{b − t h} ≤ (θ^h)^t E_b + (5/2) Mp + ∑_{(b − t h, b]} δ ,

for every t with a ≤ b − t h. The constant 5/2 is the closed geometric budget ∑_r (θ^h)^r ≤ 1/(1 − 3/5): the induction step θ^h (5/2) Mp + Mp ≤ (3/5)(5/2) Mp + Mp = (5/2) Mp is that estimate, and it is an equality at θ^h = 3/5, so the gate is used at full strength. Compare goodRunExcessIterate, which discards the weights and therefore carries the whole sum ∑_r w_{b−rh}.

The weighted run bound at the exact bottom of a run

theorem Algsuperdiff.Section4.Provider.ExcessDecay.weightedRunBound {E δ w : ℤ → ℝ} {θ κ Mp : ℝ} {h : ℕ} (hθpos : 0 < θ) (hθ1 : θ ≤ 1) (hθh : θ ^ h < 3 / 5) (hE : ∀ (k : ℤ), 0 ≤ E k) (hδ : ∀ (k : ℤ), 0 ≤ δ k) (hMp : 0 ≤ Mp) (hκ : 1 ≤ κ) (hmono : ∀ (k : ℤ), E k ≤ κ * E (k + 1)) {a b : ℤ} (hab : a ≤ b) (hwM : ∀ (j : ℤ), a ≤ j → j ≤ b → w j ≤ Mp) (hdecay : ∀ (j : ℤ), a ≤ j → j ≤ b → E (j - ↑h) ≤ θ ^ h * E j + w j + δ j) : E a ≤ (κ * θ⁻¹) ^ h * (θ ^ (b - a) * E b + 5 / 2 * Mp + ∑ j ∈ Finset.Icc a b, δ j)

The weighted good-run bound at the bottom of the run.

The iterate of weightedGoodRunIterate proves on b − t h, which overshoots the bottom a by the division remainder s = (b − a) mod h < h. Crossing those s scales with quasi-monotonicity and restoring the θ-power to the geometric θ^{b−a} costs exactly (κ θ^{-1})^h:

E_a ≤ (κ θ^{-1})^h · (θ^{b−a} E_b + (5/2) Mp + ∑_{[a,b]} δ) .

Both losses are θ-powers or κ-powers of the fixed lag h, never of the run length: that is what makes the assembly length-independent.