High-contrast homogenization: Provider.Regularity.RoundedWeakSolutionPullback #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Weak-solution transfer through the rounded normalization #
The physical equation is first put in the constant-skew gauge, then multiplied by the nonzero scalar normalizer, and finally pulled back by the rounded map.
theorem
HCPolySupport.HighContrast.isWeakSolutionOn_smul_coefficient_iff
{d : ℕ}
{U : Set (Vec d)}
(b : CoeffField d)
(F : Vec d → Vec d)
{c : ℝ}
(hc : c ≠ 0)
:
Multiplying a coefficient field by a nonzero scalar does not change its homogeneous weak-solution class.