ScaleMoment

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

Exponential moments of the minimal scale at a fixed Hölder exponent

The minimal scale of the local Hölder estimate enters the localized regularity through the factor 3^{X/2}, and the exponent at which that factor has to be integrated is a fixed multiple of gamma⁻¹. This module supplies the moment at that exponent.

The layer decomposition of 3^{cX} at a cut N0 and the exponential tail mu{X ≥ N} ≤ B e^{-θ N} give the value at the cut plus a geometric remainder. Both pieces are then evaluated for the tail

P{X ≥ N} ≤ C exp(-((1 - alpha)² (N - C)) / (C gamma)) at alpha = 1/2,

whose normal form is B = C e^{1/(4 gamma)} and θ = 1/(4 C gamma). At the exponent p = c gamma⁻¹ with

c = (4 C log 3)⁻¹,

the ratio of the geometric remainder is e^{-1/(8 C gamma)}, at most one half once gamma ≤ (8 C log 2)⁻¹; and the cut N0 = ⌈4C⌉ makes the remainder at most C, because e^{1/(4 gamma)} e^{-(N0+1)/(8 C gamma)} ≤ 1. The value at the cut is (3^{N0/2})^p, so both pieces are p-th powers of constants and the moment is a p-th power of a constant.

The exponent c depends only on the constant of the tail, hence only on the data the local Hölder estimate depends on; it does not depend on gamma.

Main results

• lintegral_homMinimalScaleFactor_le_trunc — the layer decomposition at a free cut, for a scale with a geometric tail.
• exists_minimalScaleFactor_moment_bound — ∫⁻ (3^{X/2})^{c gamma⁻¹} ≤ K^{c gamma⁻¹} for the tail of the local Hölder estimate at alpha = 1/2.

theorem Algsuperdiff.Section4.Provider.RegularityMoment.lintegral_homMinimalScaleFactor_le_trunc {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega → ℕ∞} (hX : Measurable X) {c B theta : ℝ} (N0 : ℕ) (hc : 0 ≤ c) (hB : 0 ≤ B) (htail : ∀ (N : ℕ), mu {w : Omega | ↑N ≤ X w} ≤ ENNReal.ofReal (B * Real.exp (-(theta * ↑N)))) (hratio : 3 ^ c * Real.exp (-theta) ≤ 1 / 2) : ∫⁻ (omega : Omega), Homogenization.homMinimalScaleFactor c X omega ∂mu ≤ ENNReal.ofReal (3 ^ (c * ↑N0)) + ENNReal.ofReal (2 * (B * (3 ^ c * Real.exp (-theta)) ^ (N0 + 1)))

The truncated exponential-moment engine at an arbitrary cut.

The exponential moment of 3^{cX} for a scale with the geometric tail mu{X ≥ N} ≤ B e^{-θ N} splits into the value at the cut and a geometric remainder. Unlike the packaged form used by the Theorem-B web, the cut N0 is free: the constant of the conclusion is whatever the two pieces produce.

theorem Algsuperdiff.Section4.Provider.RegularityMoment.exists_minimalScaleFactor_moment_bound {d : ℕ} (Ctail : ℝ) (hCtail : 0 < Ctail) : ∃ (gamma0 : ℝ) (c : ℝ) (K : ℝ), 0 < gamma0 ∧ 0 < c ∧ 0 < K ∧ ∀ (M : Section3.ABKModel d) (X : Section3.Cutoff.CutoffSample d → ℕ), Measurable X → M.gamma ≤ gamma0 → (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | N ≤ X omega} ≤ ENNReal.ofReal (Ctail * Real.exp (-((1 - 1 / 2) ^ 2 * (↑N - Ctail)) / (Ctail * M.gamma)))) → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (Real.rpow 3 (1 / 2 * ↑(X omega))) ^ (c * M.gamma⁻¹) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal K ^ (c * M.gamma⁻¹)

The minimal-scale factor has a bounded moment at an exponent proportional to gamma⁻¹. For a scale with the exponential tail of the local Hölder estimate at alpha = 1/2 and constant Ctail, there are a threshold, an exponent constant c and a bound K, all depending only on Ctail, such that

∫⁻ (3^{X/2})^{c gamma⁻¹} ≤ K^{c gamma⁻¹}

for every model of disorder strength at most the threshold and every scale with that tail. Both c and K are chosen before gamma.