High-contrast homogenization: Analytic.H1a0GraphClosure #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Closed-graph realization of coefficient-weighted zero-trace gradients #
The approximation clause of MemH1a0 gives unweighted gradient convergence.
Zero-trace Poincaré then makes the scalar L² representatives Cauchy, so the
smooth graph pairs converge inside the closed H¹₀ graph.
theorem
HCPolySupport.HighContrast.eLpNorm_hilbertifyVecField_eq_rpow_lintegral_vecNormSq
{d : ℕ}
{U : Set (Vec d)}
(F : Vec d → Vec d)
(hF : MeasureTheory.AEStronglyMeasurable (hilbertifyVecField F) (MeasureTheory.volume.restrict U))
:
MeasureTheory.eLpNorm (hilbertifyVecField F) 2 (MeasureTheory.volume.restrict U) = (∫⁻ (x : Vec d) in U, ENNReal.ofReal (vecNormSq (F x))) ^ (1 / 2)
The Hilbert-vector L² seminorm is the square root of the integral of
the Euclidean squared norm of the underlying vector field.
theorem
HCPolySupport.HighContrast.memVectorL2_grad_of_memH1a0
{d : ℕ}
{U : Set (Vec d)}
{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)
:
MemVectorL2 U Du
The gradient slot of a coefficient-weighted zero-trace pair has an honest
vector-valued L² realization.
theorem
HCPolySupport.HighContrast.exists_h10Function_grad_ae_eq_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)
:
∃ (w : H10Function U), w.grad =ᵐ[MeasureTheory.volume.restrict U] Du
On a bounded open convex domain, the gradient slot of a MemH1a0 pair is
the weak gradient of an actual H¹₀ function.