P4UpperMoments

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

Upper-envelope moments for the genuine cutoff

The random upper ellipticity envelope is a polynomial in the nonnegative local cutoff control. This module first exposes every finite polynomial moment of `1

• cutoffLocalControl`; later assembly may use it only through the proved samplewise bound.

theorem Algsuperdiff.Section3.Cutoff.integrable_cutoffLocalControl_pow {d : ℕ} (M : ABKModel d) (ell m : ℤ) (p : ℕ) : MeasureTheory.Integrable (fun (omega : CutoffSample d) => cutoffLocalControl ell m omega ^ p) ↑(cutoffSampleLaw M)

Every natural power of the nonnegative cutoff local control is integrable under its actual lower-tail law.

theorem Algsuperdiff.Section3.Cutoff.integrable_one_add_cutoffLocalControl_pow {d : ℕ} (M : ABKModel d) (ell m : ℤ) (p : ℕ) : MeasureTheory.Integrable (fun (omega : CutoffSample d) => (1 + cutoffLocalControl ell m omega) ^ p) ↑(cutoffSampleLaw M)

Every natural power of 1 + cutoffLocalControl is integrable. The proof uses the finite binomial expansion, so no informal closure-under-polynomials principle is assumed.

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffUpperEllipticityMajorant {d : ℕ} (M : ABKModel d) : ℝ

A deterministic polynomial majorant for the actual random upper ellipticity constant on a cube. It is deliberately stated in terms of the same local control that has the Γ₂ tail.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffUpperEllipticityMajorant M = (↑d * ↑d * (M.nu + 1) ^ 2 + M.nu ^ 2) / M.nu

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffCubeEllipticityUpper_le_majorant {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : coefficientCutoffCubeEllipticityUpper M m omega Q ≤ cutoffUpperEllipticityMajorant M * (1 + cutoffLocalControl (cubeOriginCoverScale Q) m omega) ^ 2

theorem Algsuperdiff.Section3.Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow {d : ℕ} (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) (p : ℕ) : MeasureTheory.Integrable (fun (omega : CutoffSample d) => coefficientCutoffCubeEllipticityUpper M m omega Q ^ p) ↑(cutoffSampleLaw M)

Every finite moment of the realised upper ellipticity constant on a fixed cube is integrable. This is the exact Γ₂-to-polynomial step required for the upper (P4) moment.