Coarse-graining support: Support.Book.Ch05.Theorems.Section51.AnnealedConvergence

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

Theorem t.annealed.convergence

The main theorem combines the perturbative entry mechanism with the small-contrast algebraic iteration, applied after shifting the (P4) exponents by the Section 5.3 fluctuation buffer.

def HCPolySupport.Book.Ch05.Section51.unitCoordinateVector {d : ℕ} [NeZero d] : Vec d

The first coordinate unit vector, used to test annealed response bounds in a fixed unit direction.

Equations

• HCPolySupport.Book.Ch05.Section51.unitCoordinateVector = Pi.single 0 1

theorem HCPolySupport.Book.Ch05.Section51.annealedConvergence_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ) (α : ℝ), 0 < C ∧ 0 < α ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ (n : ℕ), thetaAtScale hP hStruct ↑(annealedAlgebraicEntryScale P hP4 C + n) ≤ 1 + Real.rpow 3 (-α * ↑n)

Theorem t.annealed.convergence: convergence of the annealed contrast.

The constants are selected from the quantitative ellipticity parameter record before the probability law, hence are independent of the law itself.