High-contrast homogenization: Provider.Regularity.AffinePullbackCoeffSpaceEquiv #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Invertibility of the affine coefficient-space pullback #
The literal divergence-form pullback is reversible on the existing almost-everywhere coefficient quotient. This gives the exact carrier equivalence needed to transport families without choosing representatives.
theorem
HCPolySupport.HighContrast.affineCoefficient_inv_affineCoefficient
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
(b : CoeffField d)
(x : Vec d)
:
Pulling a coefficient field back by L and then by L⁻¹ returns the
original field pointwise.