High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorComposition.CertificatePositiveDefiniteness
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
What the reconciled-smallness certificate hands the deterministic holes #
Two of the three premises of the C¹ slope approximation at the exact-gauge terminal are discharged from the certificate itself; only the exact-gauge terminal remains.
theorem
HCPolySupport.HighContrast.CorrectorComposition.rootGoodScaleAt_posDef
{d : ℕ}
[NeZero d]
{g c kappaRate : ℝ}
{abar : Mat d}
{a : CoeffSpace d}
{x : ℝ}
(h : rootGoodScaleAt d g c kappaRate abar a x)
:
Matrix.PosDef (symmPart abar)
The c-parameterised certificate carries the positive-definiteness of the
homogenized symmetric part, exactly as RootInterface.RootGoodScale does.