High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessFluxDefectRow
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The composed row hFdefect #
memVectorL2_physical_flux_difference needs an AEUniformlyEllipticField
representative of the gauge coefficient, which exists_gaugeReducedSource
supplies for exactly the aHat premise. The shape difference — (aHat − 1) ∇u
against aHat ∇u − ∇h — is closed by sub_matVecMul and matVecMul_one at
h := u, as predicted.
theorem
HCPolySupport.HighContrast.RowSupply.frozenWitness_fluxDefect_memVectorL2
{d : ℕ}
{abar : Mat d}
(hS : Matrix.PosDef (symmPart abar))
{U : Set (Vec d)}
{j : ℤ}
{z : Vec d}
{epsilon : ℝ}
{a : CoeffSpace d}
(hepsilon : 0 < epsilon)
(hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j))
{aHat : CoeffField d}
(haHat :
aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (x : Vec d) => scaledCoeff epsilon a x - skewPart abar)
(uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U))
:
Row hFdefect. The gauge flux defect of the frozen witness is
square-integrable on the gauge domain.