Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.OneStepContraction.ResponseMoment

Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.ResponseMoment #

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

Unit-scale response moment bridge #

This file proves the local bridge used in the one-step contraction proof: for the special vectors at scale m, the unit-cube L^ζ response moment is controlled by the unit-scale (P4) ellipticity moment weight with the matched normalizations sigma^{-1} Lambda + sigma lambda^{-1}.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationResponseMomentAtScale_zero_le_unitMomentWeightAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : Ch02.vecNorm e = 1) :
Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 0 m e ≤ Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m

Unit-scale response-moment bridge for the special vectors in the one-step proof. The constant is 1; the important point is that the normalizations remain matched as \widehat\sigma_m^{-1} \Lambda + \widehat\sigma_m \lambda^{-1}.

source
theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationUnitMomentWeight_mul_responseMoment_zero_le_sq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : Ch02.vecNorm e = 1) :
Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale hP hStruct hP4 0 m e ≤ Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m ^ 2

Product form of the unit-scale response-moment bridge, matching the positive-excess term in the Section 5.3 RHS.