ValueSlotMoment #

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

B6, second half: the mean-value tail of the `L`-free value slot #

Nothing here imports that file, and nothing here claims the anchor.

What this module does #

ShellSlotBounds.lFreeValueSlot m T R ω has exactly two summands:

‖k_m − k_{j−2}‖_{L∞(3^j v + □_j)}                                     (the L∞ leg)
  +  centeringConst d · 3^{2m} · T m 0 ω                             (the mean-value tail)

with j = R.scale. Consequently

centeringConst d · 3^{2m} · tailSeriesGauge m m 0
    = 𝒪_{Γ₂}( centeringConst d · gammaTriangleConst 2 · (1 − 3^{γ−1})^{-1} · 3^{γ m} ) ,

which is the Step-4 target shape 𝒪_{Γ₂}(^{γ m}) for this summand, with an explicit constant and no exponent moved.

The domination tailSeriesGauge m m 0 ≤ deepGradSeries m 0 is proved sample, not almost surely: the two ℤ-indexed families differ by the single layer i = m, so they are summable together, and on the non-summable set both real tsums are 0. No a.e. hypothesis is therefore needed, which is what lets the conclusion be a genuine IsBigOWith (a statement about the whole measure).

References #

ABK26, (e.km.kn.Linfty, e.km.kn.Linfty.smallcube), (e.k.ell.upscales.infty), (Step 3).

1. The mean-value tail is a sub-block of the deep block #

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.tailSeriesGauge_le_deepGradSeries {d : ℕ} (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) :

tailSeriesGauge m m 0 omega ≤ deepGradSeries m 0 omega

The mean-value tail is dominated by the deep block sample.

2. The `Γ₂` display of the mean-value tail #

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.centeringConst_nonneg (d : ℕ) :

0 ≤ Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isBigOWith_gammaSigma_valueSlotMeanValueTail {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) :

HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Section3.Cutoff.CutoffSample d) => Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d * (3 ^ (2 * m) * tailSeriesGauge m m 0 omega)) (Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d * (deepGradConst M * Real.rpow 3 (M.gamma * ↑m)))

B6, second half (the settled summand): the mean-value tail of the value slot has the Step-4 target shape.

centeringConst d · 3^{2m} · tailSeriesGauge m m 0 = 𝒪_{Γ₂}(^{γ m}) with the explicit constant C = centeringConst d · gammaTriangleConst 2 · (1 − 3^{γ−1})^{-1}. No exponent is moved.

source