Coarse-graining support: Support.Book.Ch05.Theorems.Section55.ShiftedWidetildeTheta.Final #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaBound_homogenizationScale
{d : ℕ}
[NeZero d]
(xi : ℕ)
(β : ℝ)
(hβ : 0 < β)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P),
hP4.xi = xi →
Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 = β →
∀ {k n : ℕ},
k ≤ n →
thetaAtScale hP hStruct ↑n ≤ shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * β) ∧ shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * β) ≤ thetaAtScale hP hStruct ↑k + C * Real.rpow 3 (-β * ↑(n - k)) * widetildeThetaAtScale P 0 hP4
Section 5.5 shifted localization for the high-moment ellipticity contrast.
The constant is chosen after the explicit manuscript parameters xi and β,
and before the law, structural hypotheses, and window [k,n].