SuperdiffusiveBounds

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

Arithmetic assembly of the quenched displacement bounds

This file isolates the deterministic last step in the proof of ABK26, Proposition p.displacement.superdiffusive.bounds. The two results below are conditional helpers whose hypotheses are the component process estimates.

For the directional second moment, the named inputs are precisely the stopped estimate, the second-moment removal estimate, the comparison of the effective diffusivity with the intrinsic scale, and the rare-exit estimate. For the squared mean, the named inputs are the stopped squared-mean estimate and the squared form of mean removal. The conclusions retain every numerical coefficient, so a later application can choose one common constant without hiding arithmetic in an unnamed hypothesis.

The final section records the factor conversion used in the annealed estimate. In particular, the square of sqrt p + sqrt |log gamma| is bounded by the explicit factor 2 * (p + |log gamma|); the two factors are not absorbed into an unspecified constant.

References

• ABK26, Proposition p.displacement.superdiffusive.bounds, displays e.second.moment.ThmA and e.displacement.squared.ThmA.

1. Small powers of the disorder parameter

2. The directional second moment

theorem Algsuperdiff.Section5.Provider.abs_fullSecondMoment_sub_two_mul_intrinsicSq_le_of_components {gamma fullSecondMoment stoppedSecondMoment sigmaTime intrinsicSq scaleSq EB Cstopped Cremove Cscale exitProbability : ℝ} (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (hscaleSq : 0 ≤ scaleSq) (hsigmaTime_le : sigmaTime ≤ scaleSq) (hCremove : 0 ≤ Cremove) (hexitProbability : 0 ≤ exitProbability) (hstoppedSecondMoment : |stoppedSecondMoment - 2 * sigmaTime| ≤ Cstopped * scaleSq * EB + 2 * sigmaTime * exitProbability) (hsecondMomentRemoval : |fullSecondMoment - stoppedSecondMoment| ≤ Cremove * gamma ^ 50 * scaleSq) (hintrinsicScale : |intrinsicSq - sigmaTime| ≤ Cscale * √gamma * |Real.log gamma| * scaleSq) (hearlyExit : exitProbability ≤ gamma ^ 100) : |fullSecondMoment - 2 * intrinsicSq| ≤ (Cstopped * EB + (Cremove + 2 + 2 * Cscale) * (√gamma * |Real.log gamma|)) * scaleSq

The deterministic assembly of the stopped, removal, scale-comparison, and rare-exit estimates.

Here fullSecondMoment is the directional second moment at time t, stoppedSecondMoment is its stopped counterpart, sigmaTime is sigmaBar_m * t, intrinsicSq is the square of the intrinsic scale, and scaleSq is 3^(2m). The four named hypotheses are exactly the four estimates combined in the printed proof. The conclusion is the printed first display, with all constants exposed.

3. The squared mean

theorem Algsuperdiff.Section5.Provider.vecNormSq_fullMean_le_of_stopped_and_removal {d : ℕ} {gamma scaleSq EB Cstopped Cremove : ℝ} {fullMean stoppedMean : HCPolySupport.Vec d} (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (hscaleSq : 0 ≤ scaleSq) (hCremove : 0 ≤ Cremove) (hstoppedMean : HCPolySupport.vecNormSq stoppedMean ≤ Cstopped * scaleSq * EB ^ 2) (hmeanRemovalSquared : HCPolySupport.vecNormSq (fullMean - stoppedMean) ≤ Cremove * gamma ^ 100 * scaleSq) : HCPolySupport.vecNormSq fullMean ≤ (2 * Cstopped * EB ^ 2 + 2 * Cremove * gamma ^ 80) * scaleSq

The deterministic assembly of the stopped squared-mean estimate and the squared form of the mean-removal estimate.

The vectors are the full and stopped means. The conclusion displays separately the two constants multiplying EB^2 and gamma^80; a later application may replace both by one common constant.

4. The annealed moment factor

theorem Algsuperdiff.Section5.Provider.sq_sqrt_add_sqrt_abs_log_le_two_mul_add {p gamma : ℝ} (hp : 0 ≤ p) : (√p + √|Real.log gamma|) ^ 2 ≤ 2 * (p + |Real.log gamma|)

Squaring the first annealed factor produces the second, up to the explicit coefficient 2.