High-contrast homogenization: Provider.Regularity.ConstantMatrixDualIdentityReduction #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Identity-coefficient reduction of a constant-matrix dual problem #
The constant-matrix dual equation can be read as an identity-coefficient Dirichlet problem after moving the coefficient defect to the datum. This is the exact algebraic reduction needed before a small matrix perturbation can be combined with the identity-coefficient positive Besov estimate.
theorem
HCPolySupport.HighContrast.memVectorL2_constMatrix_mul
{d : ℕ}
(A : Mat d)
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : MemVectorL2 U f)
:
MemVectorL2 U fun (x : Vec d) => matVecMul A (f x)
A fixed matrix preserves vector-valued L² membership.