High-contrast homogenization: Analytic.H1a0ToH10 #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Realizing coefficient-weighted zero-trace pairs as H¹₀ functions #
The closed-graph gradient realization is identified with the original scalar
slot by comparing the same compactly supported approximants in L² and L¹.
The resulting representative is then repackaged with the original scalar and
gradient functions as its literal fields.
theorem
HCPolySupport.HighContrast.exists_h10Function_of_memH1a0
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{b : CoeffField d}
{lam Lam : ℝ}
(hlam : 0 < lam)
(hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x))
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
(hu : MemH1a0 b U u Du)
:
On a bounded open convex domain, every coefficient-weighted zero-trace
pair is represented, with its literal scalar and gradient fields, by an actual
H¹₀ function.