High-contrast homogenization: Provider.Quenched.QuenchedMainBridge

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The bridge to the inlined quenched-convergence statement

The composed quenched minimal scale is stated with the provider-tier row quenched_block_row and with a single tolerance selected before the law. The source-facing statement writes the row out in the vocabulary of the setup layer, indexes it by an integer generation, and offers every tolerance in (0,1).

Two conversions are recorded. The first is the meaning identity: above a random scale that is at least one, the integer generation is nonnegative, and the provider row at that generation is exactly the weighted sum of largest normalized coarse-block excesses restricted to the burnt-source branch. The second is the tolerance inflation: dilating the random scale by a deterministic factor trades the ratio's algebraic weight against the row's coefficient and leaves the tail of the dilated scale unchanged, the dilation being absorbed into the polynomial length.

The inlined row

noncomputable def HCPolySupport.HighContrast.Quenched.inlinedRow {d : ℕ} (rho : ℝ) (Abar : BlockMat d) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) (m : ℤ) : ℝ

The weighted row of normalized coarse-block excesses at an integer generation, written in the vocabulary of the setup layer.

Equations

• One or more equations did not get rendered due to their size.

The tolerance inflation

noncomputable def HCPolySupport.HighContrast.Quenched.toleranceDilation (kappa delta0 delta : ℝ) : ℝ

The deterministic dilation factor that trades the algebraic weight of the ratio against the coefficient of the row.

Equations

• HCPolySupport.HighContrast.Quenched.toleranceDilation kappa delta0 delta = max 1 ((delta0 / delta) ^ kappa⁻¹)

The annealed sandwich of the rebased limit block

theorem HCPolySupport.HighContrast.Quenched.annealedLimitBlock_sandwich_of_covariance {d : ℕ} [NeZero d] {P Pbase : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Pbase] {g gBase : ℝ} {E Ebase : BlockMat d} {Psi PsiBase : ℝ → ℝ} {K Kbase : ℝ} {S Sbase : CoeffSpace d → ℝ} {nBase : ℕ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Psi K S) (hstatBase : IsStationaryLaw Pbase) (hdagBase : CoarseEllipticityDagger Pbase gBase Ebase PsiBase Kbase Sbase) (hcov : ∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) : (∀ (m : ℕ), BlockMatLoewnerLE (annealedLimitBlock Pbase) (annealedBlock P (centeredCube d ↑m))) ∧ ∀ (m : ℕ), BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d ↑m))) (annealedLimitBlock Pbase)

The rebased annealed limit block is pinned by the Euclidean annealed blocks of the original law at every nonnegative generation. Above the rebase depth this is the covariance identity followed by the limit's two orderings; below it, the mean order of p.fixed.geometry.parent.child.recurrence on the original law for the lower comparison, and the greatest-lower-bound property of the limit applied to the annealed primal-adjoint order for the upper one.

The bridge

theorem HCPolySupport.HighContrast.Quenched.quenched_convergence_of_coupled_providers (d : ℕ) (hd : 2 ≤ d) (hprov : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (cSrc : ℝ) (kappa : ℝ) (delta : ℝ), 0 < C ∧ 0 < cSrc ∧ 0 < kappa ∧ delta ∈ Set.Ioo 0 1 ∧ ∀ (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) (Nann : ℕ) (Lpoly : ℝ) (Ssrc : CoeffSpace d → ℝ) (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) ∧ (∀ (a : CoeffSpace d), Ssrc a = max 1 (S a / 3 ^ Nann)) ∧ 1 ≤ Lpoly ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ Measurable Ssrc ∧ (∀ (a : CoeffSpace d), 1 ≤ Ssrc a) ∧ 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, HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta Abar S X a) : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ) (kappa : ℝ) (cSrc : ℝ), 1 < C ∧ 0 < kappa ∧ 0 < cSrc ∧ ∀ delta ∈ Set.Ioo 0 1, ∃ (Cdel : ℝ), 1 ≤ Cdel ∧ ∀ (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) ^ Cdel ∧ 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) ≤ delta * (3 ^ m / X a) ^ (-kappa)

The composed quenched minimal scale gives the inlined quenched convergence. The hypothesis is the conclusion of the coupled step, carrying in addition the two Loewner comparisons that pin the limit block against the Euclidean annealed blocks of the law itself.