High-contrast homogenization: Provider.Quenched.SmallContrastTerminalComparability

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

The terminal reference comparability

The deterministic comparability consumed by the caps: the Dagger reference is dominated by the terminal adapted mean with the factor κ_𝐄 · C(K) · boundaryConst · 3^{gG}. The chain is window-free: the annealed envelope bounds the terminal mean by the scaled reference, the sharp reverses the order, the annealed block dominates its own sharp, and the reference is dominated by κ_𝐄 times its sharp. This is the formalizable content of the printed 𝐄-preliminaries at the terminal scale.

theorem HCPolySupport.HighContrast.Quenched.adaptedCellAt_zero {d : ℕ} (q : Mat d) (t : ℤ) : adaptedCellAt q t 0 = adaptedCell q t

The zero-aligned cell is the adapted cell itself.

theorem HCPolySupport.HighContrast.Quenched.terminal_reference_comparability {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (t : ℤ) {G : ℕ} (hDelta : 0 ≤ t + ↑G - 1 - sK) (hsub : adaptedCell (roundedGrid l n) t ⊆ centeredCube d (t + ↑G)) (hint : HasFiniteAdaptedMean P (roundedGrid l n) t) : 1 ≤ kappaRef E * (sourceMomentOne K * boundaryConst Cd g n * 3 ^ (g * (↑(t + ↑G) - ↑t))) ∧ ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kappaRef E * (sourceMomentOne K * boundaryConst Cd g n * 3 ^ (g * (↑(t + ↑G) - ↑t))) * blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid l n) t) X)

The terminal reference comparability. The reference quadratic form is dominated by κ_𝐄 · C(K) · boundaryConst · 3^{gG} times the terminal mean's quadratic form.