High-contrast homogenization: Provider.Regularity.H1aGradientL2 #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Vector-valued local L² control for H¹_a gradients #
On a bounded domain, the class-honesty theorem gives integrability of
the Euclidean squared norm of the gradient slot of MemH1a. This module
packages that fact as the vector-valued L² carrier used by finite-cube PDE
interfaces.
theorem
HCPolySupport.HighContrast.memVectorL2_grad_of_memH1a
{d : ℕ}
{V : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hlam : 0 < lam)
(hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x))
(hVb : Bornology.IsBounded V)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
(hu : MemH1a b V u Du)
:
MemVectorL2 V Du
The gradient slot of a coefficient-weighted pair on a bounded domain has
an honest vector-valued L² realization.