High-contrast homogenization: Provider.Response.ConstantSkewSolenoidal #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Constant skew matrices and potential fields #
A constant skew matrix maps the weak gradient of an H¹ function to a
solenoidal field. The proof tests first against a smooth compactly supported
function. Weak integration by parts moves one derivative onto that test, and
the resulting contraction of a skew matrix with its symmetric Hessian
vanishes. Density of smooth tests then gives the Sobolev statement.
theorem
HCPolySupport.HighContrast.Response.memVectorL2_constMatrix_mul_gradient
{d : ℕ}
{U : Set (Vec d)}
(h : Mat d)
(u : H1Function U)
:
MemVectorL2 U fun (x : Vec d) => matVecMul h (u.grad x)
A constant matrix maps an L² Sobolev gradient to an L² vector field.
theorem
HCPolySupport.HighContrast.Response.isSolenoidalOn_constSkew_mul_gradient
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpen U)
(h : Mat d)
(hh : IsSkewMat h)
(u : H1Function U)
:
IsSolenoidalOn U fun (x : Vec d) => matVecMul h (u.grad x)
Multiplication of a weak gradient by a constant skew matrix gives a solenoidal field.