High-contrast homogenization: Provider.Regularity.PrintOrderParametricRoundedConstructor #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Rounded references at an arbitrarily prescribed tolerance #
Increasing the rounding generation makes the normalized-root error arbitrarily small. The resulting inverse-grid congruence is therefore positive definite, lies in the requested near-identity ellipticity window, and has operator-norm defect bounded by that tolerance.
theorem
HCPolySupport.HighContrast.exists_printOrderRoundedReferenceConstructorAtTolerance
(d : ℕ)
[NeZero d]
{eps : ℝ}
(heps0 : 0 < eps)
(hepsHalf : eps ≤ 1 / 2)
:
Every positive tolerance at most one half is attained by one rounding generation, uniformly over all positive-definite reference matrices.