Coarse-graining support: Support.Book.Ch05.Theorems.Section54.GoodScale.Assembly #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Assembly of the good-scale parameter bounds #
This file assembles the scalar monotonicity, (P4)-supplied integrability, and
special-vector algebra into the manuscript-facing good-scale lemma.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.goodScaleParameterBounds_homogenizationScale
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
(m : ℕ)
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have p0_e := (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ • q_e - p_e;
have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e;
Ch02.vecNorm ((sigmaHatAtScale hP hStruct ↑m).rpow (1 / 2) • p0_e) = |√(thetaAtScale hP hStruct ↑m) - 1| ∧ Ch02.vecNorm ((sigmaHatAtScale hP hStruct ↑m).rpow (-(1 / 2)) • q0_e) = |√(thetaAtScale hP hStruct ↑m) - 1| ∧ |√(thetaAtScale hP hStruct ↑m) - 1| ≤ √(thetaAtScale hP hStruct 0) ∧ (sigmaHatAtScale hP hStruct ↑m)⁻¹ * hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * √(thetaAtScale hP hStruct 0) ∧ sigmaHatAtScale hP hStruct ↑m * (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * √(thetaAtScale hP hStruct 0) ∧ ∀ k ≤ m,
Ch04.annealedResponseJAtScale P (↑k) p_e q_e ≤ (1 + delta) * √(thetaAtScale hP hStruct 0) ∧ tauAtScale P (↑m) (↑k) p_e q_e ≤ delta * √(thetaAtScale hP hStruct 0)
Section 5.4 good-scale parameter bounds. At a scale where both scalar coefficient chains are nearly stationary, the special vectors have controlled centering, response, and additivity defect bounds.