High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.OuterC0MatrixScaleIdentity

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

The matrix scale of the outer Dirichlet constant

The residual affine filling coefficient contains the absolute scalar scale of the symmetric reference matrix. This file makes that dependence explicit.

theorem HCPolySupport.HighContrast.RowSupply.epsilonAffineGrid_inv_mul_normalizedRoot_eq {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : (epsilonAffineGrid epsilon abar)⁻¹ * Selection.normalizedRoot (symmPart abar) = (epsilon * √(specBound (symmPart abar)⁻¹)) • 1

The cross-grid matrix in the observation filling is a scalar multiple of the identity. Its scalar is the residual dilation times the absolute normalization scale of the symmetric reference matrix.

theorem HCPolySupport.HighContrast.RowSupply.norm_epsilonAffineGrid_inv_mul_normalizedRoot {d : ℕ} [NeZero d] {epsilon : ℝ} (hepsilon : 0 < epsilon) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : ‖(epsilonAffineGrid epsilon abar)⁻¹ * Selection.normalizedRoot (symmPart abar)‖ = epsilon * √(specBound (symmPart abar)⁻¹)

Consequently, the norm entering the filling coefficient retains the same absolute normalization scale.

theorem HCPolySupport.HighContrast.RowSupply.observationFillingCoefficient_eq_absoluteScale {d : ℕ} [NeZero d] {epsilon : ℝ} (hepsilon : 0 < epsilon) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : observationFillingCoefficient d epsilon abar = max 1 (6 * ↑d * √↑d * (epsilon * √(specBound (symmPart abar)⁻¹)))

Exact expansion of the matrix-dependent observation coefficient.