High-contrast homogenization: Provider.PolynomialHomogenization.CorrectorEquationFamilyComposition #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Canonical scalar-reference corrector equation composition #
This module composes the available local Cauchy, joint-equation, global representative, and global-equation results. It records the complete same-family conclusion available before affine transport to a physical coefficient sample.
theorem
HCPolySupport.HighContrast.NormalizedLocalH1Carrier.hasWeakGradientOn_globalRepresentatives
{d : ℕ}
(z : NormalizedLocalH1Carrier d)
:
The canonical global representatives of a normalized local carrier form a genuine weak-gradient pair on all of Euclidean space.