High-contrast homogenization: Provider.PolynomialHomogenization.HomogenizedBlockIdentification

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

Identification of the homogenized coefficient matrix

The two-sided annealed sandwich pins the limiting doubled block between every finite-volume block and its sharp. Decay of the annealed contrast makes the finite-volume block and its sharp asymptotically indistinguishable. Sharp order reversal therefore forces the limiting block to be self-dual. Its canonical factorization then supplies the positive symmetric part and the skew part of the homogenized coefficient matrix.

theorem HCPolySupport.HighContrast.exists_homogenizedCoeffMatrix_of_annealedBlock_sandwich {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {Abar : BlockMat d} {Nann : ℕ} {alpha : ℝ} (hAbarSymm : IsSymmetricBlockMat Abar) (hAbarPos : Book.Ch02.BlockPosDef Abar) (hlower : ∀ (m : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑m))) (hupper : ∀ (m : ℕ), BlockMatLoewnerLE (blockSharp (annealedBlock P (centeredCube d ↑m))) Abar) (halpha : 0 < alpha) (hcontrast : ∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) : ∃ (abar : Mat d), Matrix.PosDef (symmPart abar) ∧ Book.Ch02.constantBlockMatrix abar = Abar

The annealed limit block pinned by the two-sided finite-volume sandwich is the constant doubled block associated with a homogenized coefficient matrix. The positive symmetric part and the exact doubled-block identity are produced simultaneously.