High-contrast homogenization: Provider.Regularity.LiouvilleGradientUniqueness #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Weak-gradient uniqueness for the Liouville local class #
Reverse Liouville classification identifies scalar representatives almost
everywhere. This module upgrades such an identity to the corresponding
global gradient identity, using the local integrability supplied by local
uniform ellipticity and MemH1sLoc.
theorem
HCPolySupport.HighContrast.gradient_ae_eq_of_memH1sLoc_of_value_ae
{d : ℕ}
[NeZero d]
{b : CoeffField d}
(hb : IsAELocallyUniformlyElliptic b)
{u v : Vec d → ℝ}
{Du Dv : Vec d → Vec d}
(hu : MemH1sLoc b u Du)
(hv : MemH1sLoc b v Dv)
(huv : u =ᵐ[MeasureTheory.volume] v)
:
Du =ᵐ[MeasureTheory.volume] Dv
Two MemH1sLoc pairs for a locally uniformly elliptic coefficient field
whose scalar representatives agree almost everywhere have globally
almost-everywhere equal weak-gradient representatives.