High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.AffineRateAbsorption
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.affineRate_absorption
{d : ℕ}
[NeZero d]
{S : Mat d}
(hS : Matrix.PosDef S)
{kappa x r : ℝ}
(hKappa : 0 < kappa)
(hx : 0 < x)
(hr : 0 < r)
{m : ℤ}
(hrm : r ≤ 3 ^ m)
:
√(h1AffineFactor (Selection.normalizedRoot S)) * (3 ^ m / x) ^ (-kappa) ≤ √↑d / Transport.roundedOuterResponseAffineConstant d * (r / (roundedAffineMultiplier (Transport.roundedOuterResponseAffineConstant d) (specBound S * specBound S⁻¹) kappa * x)) ^ (-kappa)
The affine negative-one loss is paid exactly by the multiplier retained between the targeted certificate scale and the common root scale.