ShellIncrementCap

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

The signed shell increment of e.what.do.we.have, and its absolute cap

The quantity

  A_{n, n+h}  =  (log 3) cstar shom_n^{-2} sum_{k = n+1}^{n+h} 3^{2 cgamma k}

is the signed drift printed in both lines of e.what.do.we.build --- more precisely of e.what.do.we.have --- and is exactly shom_n^{-2} times the A_{n,m} of e.A.def which l.integrate.approx.recurrence consumes.

This module proves the one quantitative fact about it that Step 6 needs: on the manuscript's own shell budget h <= 6 cstar cgamma^{-1}, and using the lower branch of e.shom.h.bounds carried by Algsuperdiff.Frozen.Section3.inductionState, the drift is bounded by an absolute constant, free of the model, the scale, cgamma, cstar and h:

  A_{n, n+h}  <=  36 (log 3) 3^18  =  shellIncrementCap .

The cap is what lets Closure.StepSixArithmetic.ratio_le_of_switch_upper fold the cross term delta * A of the switch factor into the printed flat error C E^2 |log cgamma|^2 cgamma. It is used on the upper branch only; the lower branch drops the same cross term by its sign and needs no cap.

The proof spends the repository's own absolute bound cstar <= 3/2 (Provider.Disorder.cstar_le_three_halves) to turn cgamma h <= 6 cstar into cgamma h <= 9; no lower bound on cstar is used or available.

References

• ABK26, e.what.do.we.have; e.A.def.
• ABK26, e.shom.h.bounds, via d.mathcalS.def.
• ABK26, the shell budget h <= 6 cstar cgamma^{-1}.

The drift

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellDrift {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) : ℝ

The signed shell increment of e.what.do.we.have.

shellDrift M n h is (log 3) cstar shom_n^{-2} sum_{k=n+1}^{n+h} 3^{2 gamma k} at the genuine running diffusivity.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellIncrementCap : ℝ

The absolute cap of the shell increment.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellIncrementCap = 36 * Real.log 3 * 3 ^ 18

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellIncrementCap_pos : 0 < shellIncrementCap

Nonnegativity

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellDrift_nonneg {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) : 0 ≤ shellDrift M n h

The geometric sum over one shell

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sum_shell_le (gamma : ℝ) (hgamma : 0 < gamma) (n : ℤ) (h : ℕ) : ∑ k ∈ Finset.Icc (n + 1) (n + ↑h), 3 ^ (2 * gamma * ↑k) ≤ ↑h * 3 ^ (2 * gamma * (↑n + ↑h))

Each term of the shell sum is below its top term, so the sum is below h 3^{2 gamma (n+h)}.

The cap

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellDrift_le_cap {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hstate : Frozen.Section3.inductionState M m0 E) {n : ℤ} (hn : n ≤ m0) {h : ℕ} (hh : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : shellDrift M n h ≤ shellIncrementCap

The shell increment is bounded by an absolute constant.

Binders: hstate is the induction state S(m0, E) of the manuscript (d.mathcalS.def), whose first clause is e.shom.h.bounds; hn places the reading scale in its range; hh is the manuscript's shell budget h <= 6 cstar cgamma^{-1}.

Only the lower branch of e.shom.h.bounds is used, and only through its cstar cgamma^{-1} 3^{2 gamma n} half; the nu^2 half of the max and the whole upper branch are discarded.