High-contrast homogenization: Provider.Quenched.QuenchedConvergenceDischarge #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Quenched.quenched_convergence_of_contrast_core
(d : ℕ)
(hd : 2 ≤ d)
(hcontrastCore :
∀ g ∈ Set.Ico 0 1,
∃ (cSc : ℝ),
0 < cSc ∧ ∃ (alpha : ℝ) (Cdelay : ℝ),
0 < alpha ∧ 0 ≤ Cdelay ∧ ∀ (cStar gBase : ℝ) (Pbase : MeasureTheory.Measure (CoeffSpace d)) (Ebase : BlockMat d) (PsiBase : ℝ → ℝ)
(Kbase : ℝ) (Sbase : CoeffSpace d → ℝ),
cStar ∈ Set.Ioc 0 cSc →
gBase = (1 + g) / 2 →
MeasureTheory.IsProbabilityMeasure Pbase →
IsStationaryLaw Pbase →
IsUnitRangeLaw Pbase →
CoarseEllipticityDagger Pbase gBase Ebase PsiBase Kbase Sbase →
annealedContrast Pbase 0 - 1 ≤ cStar →
blockContrast Ebase ≤ 1 + cSc →
∃ (m0 : ℕ),
3 ^ m0 ≤ (2 + aspectRatio Ebase * Kbase) ^ Cdelay ∧ ∀ (j : ℕ), annealedContrast Pbase ↑(m0 + j) - 1 ≤ 3 ^ (-alpha * ↑j))
:
∃ (cd : ℝ),
0 < cd ∧ ∀ g ∈ Set.Ico 0 1,
∃ (C : ℝ) (κ : ℝ) (cSrc : ℝ),
1 < C ∧ 0 < κ ∧ 0 < cSrc ∧ ∀ δ ∈ Set.Ioo 0 1,
∃ (Cδ : ℝ),
1 ≤ Cδ ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ)
(S : CoeffSpace d → ℝ),
MeasureTheory.IsProbabilityMeasure P →
IsStationaryLaw P →
IsUnitRangeLaw P →
CoarseEllipticityDagger P g E Psi K S →
∃ (Abar : BlockMat d) (Lpoly : ℝ) (X : CoeffSpace d → ℝ),
IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ (∀ (m : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑m))) ∧ (∀ (m : ℕ),
BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d ↑m))) Abar) ∧ 1 ≤ Lpoly ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ Cδ ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (t : ℝ),
1 ≤ t →
P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ (↑d - 2 * g)) + (Psi (cSrc * t))⁻¹) ∧ ∃ (OmegaEnd : Set (CoeffSpace d)),
MeasurableSet OmegaEnd ∧ P.real OmegaEnd = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' OmegaEnd = OmegaEnd) ∧ ∀ a ∈ OmegaEnd,
∀ (m : ℤ),
X a ≤ 3 ^ m →
(if S a ≤ 3 ^ m then
∑' (n : ℕ), 3 ^ (-((1 + 3 * g) / 4) * ↑n) * sSup {r : ℝ | ∃ (w : Fin d → ℤ), ⋯}
else 0) ≤ δ * (3 ^ m / X a) ^ (-κ)
Quenched convergence from the annealed contrast-decay endpoint.