P4 #

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

Dimension-only parameters for the cutoff `(P4)` route #

The quantitative coarse-grained ellipticity input in CoarseGraining separates its dimension-only exponent inequalities from its two genuine coefficient-law moment obligations. This file fixes the former once and for all for the actual Section 3 cutoff route. It deliberately does not assert those moments: they must be proved for coefficientCutoffLaw from the cutoff's local controls.

The choice is sUpper = sLower = 1/4 and xi = 8*d + 1. It works for every manuscript dimension d >= 2, and introduces no analytic assumption.

source

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffP4Params (d : ℕ) (hd : 2 ≤ d) :

HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticityParams d

The explicit dimension-only (P4) parameters used for actual cutoff laws. The two law-dependent integrability fields of QuantitativeCoarseGrainedEllipticity are intentionally absent here and are proved only after the local coarse-ellipticity observables are constructed.

Equations