High-contrast homogenization: Analytic.AffineH1a0 #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Affine transport of coefficient-weighted zero-trace data #
An invertible linear pullback transports the complete H¹_{a,0} class. The
compactly supported approximants are composed with the matrix map, while their
gradients and the limiting weak gradient transform by the transpose matrix.
theorem
HCPolySupport.HighContrast.memH1a0_affinePullback
{d : ℕ}
{L : Mat d}
(hL : IsUnit (Matrix.det L))
{U : Set (Vec d)}
(hU : MeasurableSet U)
{b : CoeffField d}
{lam Lam : ℝ}
(hlam : 0 < lam)
(hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x))
(hUfin : MeasureTheory.volume U ≠ ⊤)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
(hu : MemH1a0 b U u Du)
:
MemH1a0 (affineCoefficient L hL b) (matImage L⁻¹ U) (fun (y : Vec d) => u (matVecMul L y)) fun (y : Vec d) =>
matVecMul (matTranspose L) (Du (matVecMul L y))
The coefficient-weighted zero-trace class is covariant under every invertible linear change of variables.