High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1ReparameterizationCore
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Finite-to-limit reparameterization core #
The analytic construction of the corrector parameter map is separate from the two general steps recorded here: a uniform finite-tail estimate passes to its norm limit, and a linear endomorphism strictly closer than the identity is bijective in finite dimension.
theorem
HCPolySupport.HighContrast.linearMap_bijective_of_euclideanNorm_sub_identity_lt_one
{d : ℕ}
(P : Vec d →ₗ[ℝ] Vec d)
(theta : ℝ)
(htheta1 : theta < 1)
(hclose : ∀ (e : Vec d), euclideanNorm (P e - e) ≤ theta * euclideanNorm e)
:
A linear endomorphism whose pointwise distance from the identity is strictly smaller than one is bijective.