High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.RoundedAffineReplacement
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.isWeakSolutionOn_finiteAffineSolution
{d : ℕ}
[NeZero d]
(a : Book.Ch03.CoeffFamily d)
(m : ℤ)
(e : Vec d)
:
IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier
(finiteAffineSolution a m e).toH1.grad