Coarse-graining support: Support.Book.Ch05.Theorems.Section55.ShiftedWidetildeTheta.Uniform #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaAtScale_shifted_bound_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 →
shiftedWidetildeThetaAtScale P (↑n) hP4 β ≤ thetaAtScale hP hStruct ↑k + C * Real.rpow 3 (-β * ↑(n - k)) * widetildeThetaAtScale P (↑k) hP4
Uniform shifted-window version of the Section 5.5 shifted widetildeTheta
bound.
The constant is chosen after the explicit parameters xi and β, and before
the law and all scale parameters.