High-contrast homogenization: Provider.Quenched.AnnealedContrastComparison

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

The annealed block comparison from the annealed contrast

The endgame display e.algebraic.block.decay compares the Euclidean annealed blocks with the annealed limit block at the factor 1 + 6·3^{-αj}. Its scalar input is the annealed contrast Θ of e.Theta.m, not the canonical imbalance 𝔡 of e.scale.selection.canonical.metric, and the reference intermediate κ_𝐄 ≤ 1 + 6(Θ - 1) of the factor-six reference-block comparison is exactly what converts the one into the other.

The intermediate applies to every Euclidean annealed block, because the annealed primal-adjoint order puts that block above its own sharp. Combined with 𝐀_bar(□_m) ≼ 𝔡(𝐀_bar(□_m)) · 𝐀_bar, this yields the printed comparison, with the printed constant six and no further input.

Consequently the whole annealed package of the endgame — the limit block, its symmetry, its positive definiteness, both Loewner comparisons, the reindexing along the scale covariance, and the polynomial length account — rests on the single scalar clause e.algebraic.contrast.decay.

theorem HCPolySupport.HighContrast.Quenched.blockImbalance_annealedBlock_le_one_add_six_mul_annealedContrast_sub_one {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) : blockImbalance (annealedBlock P (centeredCube d m)) ≤ 1 + 6 * (annealedContrast P m - 1)

The annealed imbalance is controlled by the annealed contrast, at the printed constant six. This is the factor-six reference-block comparison read at the Euclidean annealed block, whose sharp ordering, the annealed primal-adjoint order, supplies the intermediate's hypothesis.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_annealedLimitBlock_of_annealedContrast_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {m : ℤ} (hm : 0 ≤ m) {eps : ℝ} (heps : annealedContrast P m - 1 ≤ eps) : BlockMatLoewnerLE (annealedBlock P (centeredCube d m)) (blockScale (1 + 6 * eps) (annealedLimitBlock P))

The upper half of the endgame block comparison, from the annealed contrast alone, at the printed constant six.

The endpoint from the printed contrast decay

theorem HCPolySupport.HighContrast.Quenched.exists_annealed_endpoint_of_rebased_contrast_decay {d : ℕ} [NeZero d] {P Pbase : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure Pbase] {E Ebase : BlockMat d} {Ψbase : ℝ → ℝ} {K Kbase gBase : ℝ} {Sbase : CoeffSpace d → ℝ} {alpha Crebase Cdelay Cann : ℝ} {nBase m0 : ℕ} (hstat : IsStationaryLaw Pbase) (hdag : CoarseEllipticityDagger Pbase gBase Ebase Ψbase Kbase Sbase) (hcovContrast : ∀ (j : ℕ), annealedContrast Pbase ↑j = annealedContrast P ↑(nBase + j)) (hcovBlock : ∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) (hbase : 1 ≤ 2 + aspectRatio E * K) (hnBase : 3 ^ nBase ≤ (2 + aspectRatio E * K) ^ Crebase) (hrefCost : 2 + aspectRatio Ebase * Kbase ≤ (2 + aspectRatio E * K) ^ Crebase) (hCdelay : 0 ≤ Cdelay) (hCann : Crebase * (1 + Cdelay) ≤ Cann) (hdelay : 3 ^ m0 ≤ (2 + aspectRatio Ebase * Kbase) ^ Cdelay) (hcontrast : ∀ (j : ℕ), annealedContrast Pbase ↑(m0 + j) - 1 ≤ 3 ^ (-alpha * ↑j)) : ∃ (Abar : BlockMat d) (Nann : ℕ), IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ 3 ^ Nann ≤ (2 + aspectRatio E * K) ^ Cann ∧ (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) ∧ (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) ∧ Abar = annealedLimitBlock Pbase

The annealed endpoint of the endgame from the printed contrast decay alone. The hypothesis hcontrast is e.algebraic.contrast.decay on the rebased law; the block comparison e.algebraic.block.decay is derived, not assumed.