SmallScaleBound

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

The corrected small-scale diffusivity envelope

ABK26's deterministic integration lemma assumes the all-scale estimate

nu <= s_m <= (1 + nu^(-2) cstar gamma^(-1) 3^(2 gamma m)) nu.

This file exposes that two-constant boundary directly for the genuine running diffusivity. The subsequent deterministic recurrence-integration provider can therefore consume the sound cstarPlus envelope without adding an unproved interface hypothesis.

References

• ABK26, e.small.scale.bound.
• ABK26, e.plateau.region.bound.

theorem Algsuperdiff.Section3.Provider.Diffusivity.annealedPlateau_smallScaleBound {d : ℕ} (M : ABKModel d) (m : ℤ) : M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ (1 + (M.nu ^ 2)⁻¹ * Disorder.cstarPlus M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) * M.nu

The corrected e.small.scale.bound for the genuine running diffusivity.

The envelope constant is cstarPlus, as required; this theorem does not replace the directional cstar used by the recurrence or the target profile.