P4UpperLaw

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

Upper coarse-ellipticity moments under the cutoff law

This file transfers the independently proved samplewise cutoff envelope bound and its Γ₂-derived polynomial moments through the literal cutoff pushforward.

theorem Algsuperdiff.Section3.Cutoff.integrable_LambdaSqCoeffField_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)

Every finite upper coarse-ellipticity moment on an arbitrary deterministic cube is integrable under the actual cutoff law.