PlateauLandmarks

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

The landmark specializations of the annealed plateau bound

ABK26, records two consequences of the unconditional plateau display e.basecase.shom.m. For every m below the base landmark m**,

nu Id <= shom_m <= (1 + gamma^2) nu Id (e.basecase.homogenization),

and for every m below the plateau landmark m*,

nu Id <= shom_m <= 2 nu Id (e.basecase.diffusivity).

The proof of p.base.case says these "follow immediately from e.basecase.shom.m. by using the definitions of m** and m*", and that is exactly the route taken here. This file delivers only the diffusivity conjuncts of the two displays; their homogenization-error conjuncts are the business of other modules.

Route

Write

A_m := c+ (2 nu^2)^{-1} gamma^{-1} (1 + 4 gamma) 3^{2 gamma m}

for the plateau amplitude of annealedPlateau, so that sigmaBar_m <= nu (1 + A_m) unconditionally. Both landmark characterizations have the quotient form 3^{2 gamma m} <= nu^2 w / (2 (log 3) c+), with weight w = gamma^3 at m** and w = gamma at m*. Substituting the quotient bound into A_m cancels c+ and nu^2 and leaves

A_m <= (1 + 4 gamma) w gamma^{-1} / (4 log 3) <= w gamma^{-1},

because gamma <= 1/4 gives 1 + 4 gamma <= 2 while log 3 > 1 gives 4 log 3 > 4. That single estimate is plateau_amplitude_le; the two branches are its w = gamma^3 instance (w gamma^{-1} = gamma^2) and its w = gamma instance (w gamma^{-1} = 1).

Main results

• annealedPlateau_le_mStarStar: the diffusivity conjunct of e.basecase.homogenization.
• annealedPlateau_le_mStar: the diffusivity conjunct of e.basecase.diffusivity.

References

• ABK26, e.basecase.homogenization, e.basecase.diffusivity, with the proof reference.
• ABK26, e.mstarstar, e.mstar.

The numeric input

The common landmark collapse

The two landmark displays

theorem Algsuperdiff.Section3.Provider.Base.annealedPlateau_le_mStarStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStarStar M) : M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ (1 + M.gamma ^ 2) * M.nu

ABK26, e.basecase.homogenization, diffusivity conjunct.

For every m <= m**, the annealed running diffusivity of the coefficient cutoff satisfies nu <= sigmaBar_m <= (1 + gamma^2) nu.

The lower leg is the unconditional plateau's own lower leg. For the upper leg, e.mstarstar gives 3 ^ (2 gamma m) <= nu^2 gamma^3 / (2 (log 3) c+), so the plateau amplitude is at most gamma^3 gamma⁻¹ = gamma^2.

theorem Algsuperdiff.Section3.Provider.Base.annealedPlateau_le_mStar {d : ℕ} (M : ABKModel d) (m : ℤ) (hm : m ≤ mStar M) : M.nu ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M m) ≤ 2 * M.nu

ABK26, e.basecase.diffusivity, diffusivity conjunct.

For every m <= m*, the annealed running diffusivity of the coefficient cutoff satisfies nu <= sigmaBar_m <= 2 nu.

The m* window is the wider of the two landmark windows: e.mstar gives only 3 ^ (2 gamma m) <= nu^2 gamma / (2 (log 3) c+), so the plateau amplitude is bounded by gamma gamma⁻¹ = 1, which is exactly what the printed constant 2 accommodates.