NormalizedP4

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

Exact normalized (P4) for the genuine cutoff

The normalized cutoff law is evaluated only at the canonical least depth cutoffNormalizationDepth. Its two moments are transported from arbitrary original origin-cube scales through CoarseGraining's exact dilation law.

theorem Algsuperdiff.Section3.Cutoff.integrable_scaleNormalized_LambdaSqCoeffField_pow {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (k : ℕ) {s : ℝ} (hs : 0 < s) (xi : ℕ) : MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => HCPolySupport.Book.Ch04.LambdaSqCoeffField (HCPolySupport.originCube d 0) s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a ^ xi) (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k (coefficientCutoffLaw M m))

theorem Algsuperdiff.Section3.Cutoff.integrable_scaleNormalized_lambdaSqCoeffField_inv_pow {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (k : ℕ) {s : ℝ} (hs : 0 < s) (xi : ℕ) : MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => (HCPolySupport.Book.Ch04.lambdaSqCoeffField (HCPolySupport.originCube d 0) s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ xi) (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k (coefficientCutoffLaw M m))

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffNormalizationQuantitativeCoarseGrainedEllipticity {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw (cutoffNormalizationDepth d m) (coefficientCutoffLaw M m))

Exact (P4) evidence for the canonical range-normalized genuine cutoff law. QuantitativeCoarseGrainedEllipticity is a Type-valued CoarseGraining evidence record, so this must be a definition rather than a proposition-valued theorem. No unnormalized (P4) or structural law is assumed.

Equations

• One or more equations did not get rendered due to their size.