Coarse-graining support: Support.Book.Ch05.Theorems.Section55.AnnealedConvergence #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Main annealed convergence theorem #
This file contains the scalar iteration which turns the one-step annealed improvement into the main annealed convergence theorem.
theorem
HCPolySupport.Book.Ch05.Section55.annealedPerturbativeEntry_homogenizationScale
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (C : ℝ),
0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P),
hP4.params = params →
∀ (sigma : ℝ),
0 < sigma → sigma ≤ 1 / 2 → thetaAtScale hP hStruct ↑(annealedEntryScale P hP4 C sigma) ≤ 1 + sigma
Proposition p.annealed.convergence.homogenization.scale.
The constant is chosen from the parameter record before the law and the target
accuracy. The entry scale is the manuscript two-ceiling scale from
annealedEntryScale.