High-contrast homogenization: Provider.Regularity.RoundedReferenceDualIdentityReduction #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Quantitative identity reduction for the rounded-reference dual problem #
The rounded reference matrix differs from the identity by at most one percent in operator norm. This module combines that proved geometric bound with the exact constant-matrix identity reduction, exposing both pointwise and integrated control of the resulting dual residual.
theorem
HCPolySupport.HighContrast.norm_roundedReferenceMatrix_sub_one_le
{d : ℕ}
[NeZero d]
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
:
The selected value of the rounded constant reference is within one percent of the identity in operator norm.