StepFourMoments #

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

Step 4's "hence, for every `q`": the moment reading of the proved bullets #

What this module does #

Step 4 of the proof of l.bounds.mathcal.E.aL lists the inputs of the sensitivity display and converts each into a q-th moment bound.

The bullet table, and where each conversion is:

(B1) σ_m^{-1}σ_{j−2} ≤ 4, deterministic: exists_lintegral_rpow_inv_sigmaBar_mul_sigmaBar_sub_two_le.
(B2) (σ_mσ_{j−2}^{-1}−1)² ≤ …, deterministic: exists_lintegral_rpow_sigmaBar_ratio_sub_one_sq_le.
(B3) 3^{γj}σ_{j−2}^{-1} ≤ 4c⋆^{-1/2}γ^{1/2}, deterministic: exists_lintegral_rpow_gamma_weight_inv_sigmaBar_le.
(B4) 𝓔_{s,2,2}(□_j;𝐚_{j−2},σ_{j−2}), (Γ₂,Γ_{1/2}): exists_lintegral_rpow_unitCubeHomogenizationError22_le.
(B5) λ_{γ,2}^{-1}(□_j;𝐚_{j−2}), Γ_{1/3}: NOT here -- see LambdaSlotB5.lean.
(B6a) 3^{2j}‖∇(k_L−k_{j−2})‖_{W^{1,∞}}, Γ₂: lintegral_rpow_weightedFullGradSeries_le, lintegral_rpow_lFreeGradSlot_le.
(B6b) ‖k_L−k_{j−2}−(k_L−k_m)_{□_m}‖_{L²}, Γ₂: lintegral_rpow_valueSlotLinfty_le and lintegral_rpow_valueSlotMeanValueTail_le (the two legs, kept apart).

The three deterministic bullets convert trivially: a probability measure has total mass one, so the q-th moment of a constant is the constant. The four random ones convert through l.moments.gamma.psi, whose q^{1/σ} is √q at σ = 2 (the printed q^{1/2}, and the anchor's √p) and q² at σ = 1/2 (the printed q²).

What is NOT claimed #

The two q-powers are exactly the printed ones and no exponent is moved; the constants are the explicit ones of the proved displays, which the manuscript's C(d, c⋆) convention absorbs.

References #

ABK26, l.bounds.mathcal.E.aL; l.moments.gamma.psi.

1. The three deterministic bullets #

2. (B4): the two-term bullet at the literal `(2,2)` error #

source

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

∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ s ∈ Set.Icc (8 * M.gamma) 1, ∀ (R : HCPolySupport.TriadicCube d) (p : ℝ), 1 ≤ p → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (Frozen.Section24.unitCubeHomogenizationError s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (R.scale - 2)))) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (gammaTwoHalfMomentBound p (√3 * (Proportion.annulusPenalty d 2 1 * (C * (Section3.Disorder.cstar M)⁻¹ * s⁻¹ * √M.gamma))) (√3 * (Proportion.annulusPenalty d (1 / 2) 1 * Real.exp (-(C⁻¹ * Section3.Disorder.cstar M ^ 3 * M.gamma⁻¹))))) ^ p

(B4) at every moment q ∈ [1,∞), for the literal (2,2) error.

The printed conversion is E[𝓔_{s,2,2}^q]^{1/q} ≤ C s^{-1} q^{1/2} γ^{1/2} + C q² exp(−C^{-1}γ^{-1}): the √q is the Γ₂ lane's q^{1/σ} at σ = 2 and the q² is the Γ_{1/2} lane's at σ = 1/2. Both are carried verbatim by gammaTwoHalfMomentBound.

3. (B6a): the whole `L`-free gradient slot #

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.fullGradSeries_nonneg {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) :

0 ≤ fullGradSeries k v omega

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_fullGradSeries {d : ℕ} (k : ℤ) (v : Fin d → ℤ) :

Measurable fun (omega : Section3.Cutoff.CutoffSample d) => fullGradSeries k v omega

source

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_lFreeGradSlot_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (hkm : R.scale ≤ m) {p : ℝ} (hp : 1 ≤ p) :

∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (lFreeGradSlot m (tailSeriesGauge m) R omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (gammaTwoMomentBound p (fullGradConst M * Real.rpow 3 (M.gamma * ↑R.scale))) ^ p

(B6a) at the slot itself. Almost surely the L-free gradient slot IS the weighted full series, so it inherits the moment bound. This is the form the Step-5 assembly consumes.