Coarse-graining support: Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.Final #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Proposition p.small.contrast.algebraic.decay.homogenization.scale #
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.smallContrastAlgebraicDecay_homogenizationScale
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (α : ℝ) (δ0 : ℝ) (C : ℝ),
0 < α ∧ 0 < δ0 ∧ 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P),
hP4.params = params →
widetildeThetaAtScale P 0 hP4 - 1 ≤ δ0 →
∀ (m : ℕ) (e : Vec d),
vecNormSq e = 1 →
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ C * Real.rpow 3 (-α * ↑m)
Proposition p.small.contrast.algebraic.decay.homogenization.scale.
The constants are selected from the parameter record before the probability law, so they are independent of the measure.