Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.NormalizedRootEnclosure

High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedRootEnclosure #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Enclosure bounds for the exact normalized root #

The exact identity-normalizing root has a triadic enclosure controlled by its projective eccentricity. Its inverse norm also removes the coefficient dependence from the boundary-filling factor.

source
theorem HCPolySupport.HighContrast.normalizedRoot_fillingBoundaryFactor_le {d : ℕ} (hd : 1 ≤ d) {m : Mat d} (hm : Matrix.PosDef m) :
max 1 (6 * ↑d * √↑d * ‖(Selection.normalizedRoot m)⁻¹‖) ≤ 6 * ↑d * √↑d

For the exact normalized root, the boundary-filling factor is bounded by the dimension-only factor.