Coarse-graining support: Support.Book.Ch05.Theorems.Section57.AnnealedJLimit #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Annealed bound for the limiting-normalized block response #
This file supplies the deterministic annealed input in Corollary
c.first.quenched.estimate: after the main annealed theorem has made the
scalar contrast small, the annealed response with the limiting normalization
is small as well.
theorem
HCPolySupport.Book.Ch05.Section57.abs_fullBlockVec_coord_le_one_of_dotProduct_le_one
{d : ℕ}
(e : FullBlockVec d)
(he : e ⬝ᵥ e ≤ 1)
(α : BlockCoord d)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.integral_limitNormalizedBlockJObservable_le_thetaAtScale_sub_one
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
(k : ℕ)
(e : FullBlockVec d)
(he_norm : e ⬝ᵥ e ≤ 1)
:
∫ (a : RegCoeffField d), limitNormalizedBlockJObservable hP hStruct (originCube d ↑k) e a ∂P ≤ thetaAtScale hP hStruct ↑k - 1
The annealed response with limiting scalar normalizers is controlled by the scalar contrast at the same scale.