P4Moments #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Moment transport for cutoff coarse ellipticity #
This module assembles law-level moment consequences of the verified samplewise cutoff bounds. It deliberately keeps the deterministic lower moment separate from the stochastic upper moment, whose proof must consume the actual Γ₂ control of the cutoff local envelope.
theorem
Algsuperdiff.Section3.Cutoff.integrable_lambdaSqCoeffField_inv_pow_cutoffLaw
{d : ℕ}
[NeZero d]
(M : ABKModel d)
(m : ℤ)
(Q : HCPolySupport.TriadicCube d)
{s : ℝ}
(hs : 0 < s)
(xi : ℕ)
:
MeasureTheory.Integrable
(fun (a : HCPolySupport.RegCoeffField d) =>
(HCPolySupport.Book.Ch04.lambdaSqCoeffField Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ xi)
(coefficientCutoffLaw M m)
All finite lower (P4) moments are integrable under the genuine cutoff law. This
uses only the deterministic coercivity nu; it introduces no upper-ellipticity
or structural-law hypothesis.