High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.GaugeAffineFactor
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.sqrt_H1AffineFactor_normalizedRoot_le
{d : ℕ}
[NeZero d]
{S : Mat d}
(hS : Matrix.PosDef S)
:
The normalized-root affine loss in the negative-one transport is bounded by a dimension-only factor times the witness eccentricity.