RelativeNormalizedP4

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

for the same-cutoff relative normalization

The relative law is an arbitrary integer triadic dilation, so CoarseGraining's natural-depth transport cannot be applied directly. This file proves the two exact deterministic dilation identities at an arbitrary integer exponent and transports the already established arbitrary-cube cutoff moments.

theorem Algsuperdiff.Section3.Cutoff.LambdaSqCoeffField_dilateReg_of_aelocallyUniformlyElliptic {d : ℕ} {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) (Q : HCPolySupport.TriadicCube d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : HCPolySupport.Book.Ch04.LambdaSqCoeffField Q s q (HCPolySupport.dilateReg k a) = HCPolySupport.Book.Ch04.LambdaSqCoeffField (HCPolySupport.Book.Ch02.dilateCube (-k) Q) s q a

The upper Chapter 4 multiscale observable shifts by an arbitrary integer triadic dilation.

theorem Algsuperdiff.Section3.Cutoff.lambdaSqCoeffField_dilateReg_of_aelocallyUniformlyElliptic {d : ℕ} {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (k : ℤ) (Q : HCPolySupport.TriadicCube d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : HCPolySupport.Book.Ch04.lambdaSqCoeffField Q s q (HCPolySupport.dilateReg k a) = HCPolySupport.Book.Ch04.lambdaSqCoeffField (HCPolySupport.Book.Ch02.dilateCube (-k) Q) s q a

The lower Chapter 4 multiscale observable shifts by an arbitrary integer triadic dilation.

theorem Algsuperdiff.Section3.Cutoff.integrable_relativeNormalized_LambdaSqCoeffField_pow {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) {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) (relativeNormalizedCutoffLaw M m)

theorem Algsuperdiff.Section3.Cutoff.integrable_relativeNormalized_lambdaSqCoeffField_inv_pow {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) {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) (relativeNormalizedCutoffLaw M m)

noncomputable def Algsuperdiff.Section3.Cutoff.relativeNormalizedCutoffLawQuantitativeCoarseGrainedEllipticity {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity (relativeNormalizedCutoffLaw M m)

Exact evidence for the same-cutoff relative normalization.

Equations

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