TailProbability

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

The two upper-tail conditions hold almost surely

Both conditions of TailGauge.lean are countable statements whose terms have summable first moments, so Tonelli's theorem gives them almost surely.

• The ascending gradient series on one cube y + □_n is summable almost surely because its terms have Γ₂ tails at geometric amplitudes; this is the probabilistic content of (J2) after the exact scaling law of the shells.
• The quantitative two-leg condition is the same statement for the doubly indexed family weighted by 3^{-ℓ} on the descending leg and 3^{ℓ} on the ascending leg, whose first moments are of order (3^{γ-1})^{ℓ} times a summable profile in r. Finiteness of the double sum gives one sample constant valid at every scale, which is what the growth bound of the field needs.

Main results

• ae_upperGradBounded — the ascending series on y + □_n is bounded.

References

• ABK26, (J2), e.jk.O, e.nabla.jk.O.

2. The geometric ascending amplitude

3. The ascending condition on one cube

theorem Algsuperdiff.Section5.Field.ae_upperGradBounded {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), UpperGradBounded n y omega

The ascending gradient series on y + □_n has bounded partial sums almost surely. This is (J2) read through the exact shell scaling: the r-th term has a Γ₂ tail at the geometric amplitude 3^{-n} 3^{(γ-1)(n+r)}.

4. The quantitative two-leg condition