Coarse-graining support: Support.Book.Ch05.Theorems.Section55.DilatedP4

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.upperMomentIntegrable_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) hP4.sUpper (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) (Ch04.restrictionScaleNormalizedLaw k P)

theorem HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.lowerInvMomentIntegrable_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) hP4.sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) (Ch04.restrictionScaleNormalizedLaw k P)

def HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity.scaleNormalized {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (k : ℕ) : QuantitativeCoarseGrainedEllipticity (Ch04.restrictionScaleNormalizedLaw k P)

The Chapter 5 quantitative coarse-grained ellipticity hypothesis is stable under Ch4 scale normalization. The unit-scale moment assumptions for the pushed law are exactly the arbitrary-scale moment consequences of (P4) for the original law.

Equations

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