Coarse-graining support: Support.Book.Ch05.Theorems.Section54.Pigeonhole #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Pigeonhole lemma #
This module is the public entry point for the first result of Section 5.4.
theorem
HCPolySupport.Book.Ch05.Section54.pigeonhole_homogenizationScale
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta sigma : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
(hsigma_pos : 0 < sigma)
(hsigma_le : sigma ≤ 1 / 2)
{N h : ℕ}
(hsep : ⌈2 * delta⁻¹ * |Real.log sigma|⌉₊ * h ≤ N)
:
(∃ (n : ℕ),
h ≤ n ∧ n ≤ N ∧ hP.barSigmaAtScale hStruct ↑(n - h) ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑n ∧ (hP.barSigmaStarAtScale hStruct ↑(n - h))⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑n)⁻¹) ∨ thetaAtScale hP hStruct ↑N ≤ sigma * thetaAtScale hP hStruct 0
Section 5.4 pigeonhole lemma for the annealed scalar contrast. Either
there is a scale n ∈ {h, ..., N} at which both scalar chains are nearly
stationary across the gap h, or the contrast has already contracted by
sigma.