High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.HomogenizedEccentricityBound

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

The eccentricity of the homogenized matrix is polynomial in the reference data

The homogenized coefficient matrix is pinned by a two-sided annealed sandwich, and the coarse-ellipticity assumption puts every annealed block below a scalar multiple of the reference block. The doubled block of the homogenized matrix is therefore below a scalar multiple of the reference block, and the reference aspect ratio is monotone for that order and homogeneous of degree two under the dilation.

The doubled block of a coefficient matrix has the matrix's symmetric part as its Schur block and the inverse of that symmetric part as its lower-right block, so its aspect ratio dominates the square of the witness eccentricity of the symmetric part. Composing gives a bound on the eccentricity by a fixed power of 2 + Π K, the same polynomial length datum the statement already carries.

The Schur data of a constant doubled block

theorem HCPolySupport.HighContrast.RowSupply.schurSkew_constantBlockMatrix {d : ℕ} {a0 : Mat d} (hS : Matrix.PosDef (symmPart a0)) : schurSkew (Book.Ch02.constantBlockMatrix a0) = skewPart a0

The Schur skew block of the doubled block of a coefficient matrix is the matrix's skew part.

theorem HCPolySupport.HighContrast.RowSupply.schurSigma_constantBlockMatrix {d : ℕ} {a0 : Mat d} (hS : Matrix.PosDef (symmPart a0)) : schurSigma (Book.Ch02.constantBlockMatrix a0) = symmPart a0

The Schur block of the doubled block of a coefficient matrix is the matrix's symmetric part.

theorem HCPolySupport.HighContrast.RowSupply.lowerRight_constantBlockMatrix {d : ℕ} (a0 : Mat d) : (Book.Ch02.constantBlockMatrix a0).lowerRight = (symmPart a0)⁻¹

The lower-right block of the doubled block of a coefficient matrix is the inverse of the matrix's symmetric part.

The eccentricity against the aspect ratio of the doubled block

theorem HCPolySupport.HighContrast.RowSupply.witnessEccentricity_sq_le_aspectRatio_constantBlockMatrix {d : ℕ} {a0 : Mat d} (hS : Matrix.PosDef (symmPart a0)) : witnessEccentricity (symmPart a0) ^ 2 ≤ aspectRatio (Book.Ch02.constantBlockMatrix a0)

The eccentricity is controlled by the aspect ratio of the doubled block. The Schur block contributes the spectral bound of the symmetric part, which is below the reference constant Λ_0 of the doubled block, and the lower-right block contributes the spectral bound of the inverse exactly.

The arithmetic of the polynomial length

theorem HCPolySupport.HighContrast.RowSupply.mul_le_pow_two_add_mul {c Pi K : ℝ} (hPi : 1 ≤ Pi) (hK : 1 < K) (hc : c ≤ 1 + 6 * K ^ 2) : c * Pi ≤ (2 + Pi * K) ^ 5

The closing arithmetic: a bound of the shape c ≤ 1 + 6K² on the dilation constant and 1 ≤ Π on the aspect ratio give the fifth power of the printed polynomial length datum.

The law-level bound

theorem HCPolySupport.HighContrast.RowSupply.witnessEccentricity_symmPart_le_rpow_aspectRatio {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} {Abar : BlockMat d} {abar : Mat d} (hdag : CoarseEllipticityDagger P g E Psi K S) (hS : Matrix.PosDef (symmPart abar)) (hAbarSymm : IsSymmetricBlockMat Abar) (hlower : ∀ (m : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑m))) (hAbarEq : Book.Ch02.constantBlockMatrix abar = Abar) : witnessEccentricity (symmPart abar) ≤ (2 + aspectRatio E * K) ^ 5

The homogenized eccentricity is polynomial in the reference data. The witness eccentricity of the symmetric part of the homogenized matrix is bounded by the fifth power of 2 + Π K, with an exponent independent of the law, the reference block, the gauge and the source scale.

The hypotheses are exactly the data the root assembly holds where the homogenized matrix is produced: the coarse-ellipticity assumption, the symmetry and the lower half of the annealed sandwich pinning the limiting block, and the identification of that block as the doubled block of the homogenized matrix.