AnnealedPlateau

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

ABK26's e.plateau.region.bound

ABK26, takes the expectation of e.basecase.tightbound and uses e.annealed.khom.zero and e.km.L2.expectation to obtain

nu Id <= shom_{m,*}(cu_l) <= shom_m <= shom_m(cu_l) <= nu (1 + (1/2) nu^{-2} c* gamma^{-1} (1 + 4 gamma) 3^{2 gamma m}) Id,

which is e.basecase.shom.m.

The local conclusion is the scalar pair carried by the frozen base-case statement,

nu <= sigmaBar_m <= nu (1 + c+ (2 nu^2)^{-1} gamma^{-1} (1 + 4 gamma) 3^{2 gamma m}).

Route

• Every annealed cutoff block on an origin cube is a scalar matrix (Provider.Annealed.coefficientCutoffLaw_isScalarMatrix_annealedBAtScale), and the annealed coupling matrix vanishes (Provider.Annealed.coefficientCutoffLaw_annealedKappa_eq_zero), so shom_m(cu_n) = bhom_m(cu_n) is a scalar.
• The finite-volume annealed block bhom_m(cu_n) is the expectation of the deterministic b_m(cu_n), so the deterministic chain integrates: the lower leg gives nu and the upper leg gives nu + nu^{-1} E[||k_m||^2_{L2bar(cu_n)}], with the expectation supplied exactly by Provider.Stream.integral_average_frobeniusMass_cutoff.
• The resulting two-sided bound is uniform in the cube scale n, which is what the source's monotone sandwich delivers. Passing to the limit in the unique-choice characterization Annealed.sigmaBar_characterization therefore gives the same bounds for sigmaBar_m; no separate Loewner monotonicity input is needed.
• The arithmetic step is e.K.cgamma.ineq: K_gamma <= gamma^{-1} + 4 = gamma^{-1} (1 + 4 gamma).

Main results

• integrable_average_frobeniusMass_cutoff
• coarseBlockMatrix_upperLeft_coefficientCutoff
• annealedBAtScale_entry_bounds
• annealedPlateau: the display e.basecase.shom.m.

References

• ABK26, e.plateau.region.bound, e.basecase.shom.m.
• ABK26, e.km.L2.expectation.
• ABK26, e.K.cgamma.ineq.

Integrability of the per-cube stream mass

theorem Algsuperdiff.Section3.Provider.Base.integrable_average_frobeniusMass_cutoff {d : ℕ} (M : ABKModel d) (l m : ℤ) : MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.average (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d l)) fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x)) ↑(Cutoff.cutoffSampleLaw M)

The per-cube volume-normalized L^2 mass of k_m is integrable in the cutoff sample: it is jointly measurable and dominated on cu_l by the square of the corresponding local control, whose second moment is finite.

The deterministic upper-left block

theorem Algsuperdiff.Section3.Provider.Base.coarseBlockMatrix_upperLeft_coefficientCutoff {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) (omega : Cutoff.CutoffSample d) : (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) (Cutoff.coefficientCutoff M.nu m omega).toFun).upperLeft = HCPolySupport.Book.Ch02.bCoarse (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n)) (Cutoff.coefficientCutoffCoeffOn M m omega (HCPolySupport.originCube d n))

The upper-left coarse block of the cutoff coefficient on an origin cube is the Chapter 2 derived matrix b_m(cu_n).

The annealed upper-left block

The finite-volume annealed bounds

The plateau arithmetic

The scalar finite-volume bounds and the infinite-volume limit

theorem Algsuperdiff.Section3.Provider.Base.annealedBAtScale_entry_bounds {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : M.nu ≤ HCPolySupport.Book.Ch04.annealedBAtScale (Cutoff.coefficientCutoffLaw M m) n 0 0 ∧ HCPolySupport.Book.Ch04.annealedBAtScale (Cutoff.coefficientCutoffLaw M m) n 0 0 ≤ M.nu * (1 + Disorder.cstarPlus M * (2 * M.nu ^ 2)⁻¹ * M.gamma⁻¹ * (1 + 4 * M.gamma) * 3 ^ (2 * M.gamma * ↑m))

ABK26. The finite-volume annealed diffusivity of the cutoff at every origin-cube scale n obeys the plateau bounds, uniformly in n.

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

ABK26, e.plateau.region.bound, e.basecase.shom.m.

For every m in Z,

nu <= sigmaBar_m <= nu (1 + c+ (2 nu^2)^{-1} gamma^{-1} (1 + 4 gamma) 3^{2 gamma m}),

where sigmaBar_m is the infinite-volume annealed running diffusivity of the coefficient cutoff and c+ is the canonical Frobenius shell constant of e.km.L2.expectation.