WeightedGoodRunAssembly

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

The weighted run assembly across the bad scales (decay-carrying)

ABK26, §4.3, l.iteration.lemma, Step 3 in the decay-carrying bookkeeping that conclusion (ii) (e.excess.decay.lemma) needs, for abstract nonnegative sequences.

IterationLemma.assembleRuns concatenates the good runs of ([n,m] ∩ ℤ) ∖ B keeping the error terms and discarding the geometric decay. weightedAssemble does the opposite: it keeps a genuine θ^{m−k} on the top excess, and pays for it with

• one factor Λ = 2(κθ^{-1})^{h+2} per bad scale crossed, plus one for the initial run;
• a single error budget (5/2)·Mp + ∑_{[k,m]} δ --- length-independent, because weightedRunBound is length-independent and the factor 2 inside Λ absorbs the one extra copy each crossing produces.

E_k ≤ Λ^{|B ∩ [k,m]| + 1} · (θ^{m−k} E_m + (5/2) Mp + ∑_{[k,m]} δ) .

The θ-payback θ^{-(h+2)(|B ∩ [k,m]|+1)} hidden inside Λ^{|B∩[k,m]|+1} is exactly the division remainder plus the crossings, and it is dominated by the frozen statement's θ^{-C(h+1)(|B|+1)} for every C ≥ 2; the κ-growth is carried by the exp factor.

References

• ABK26, l.iteration.lemma Step 3; conclusion (ii).

Absorption helpers (pure algebra over abstract reals)

The assembly

theorem Algsuperdiff.Section4.Provider.ExcessDecay.weightedAssemble {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)) {n m : ℤ} (B : Finset ℤ) (hwM : ∀ (j : ℤ), n ≤ j → j ≤ m → w j ≤ Mp) (hdecay : ∀ (j : ℤ), n ≤ j → j ≤ m → j ∉ B → E (j - ↑h) ≤ θ ^ h * E j + w j + δ j) (k : ℤ) : n ≤ k → k ≤ m → E k ≤ (2 * (κ * θ⁻¹) ^ (h + 2)) ^ ((B ∩ Finset.Icc k m).card + 1) * (θ ^ (m - k) * E m + 5 / 2 * Mp + ∑ j ∈ Finset.Icc k m, δ j)