High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.LiouvilleAECongruence
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Almost-everywhere congruence for the Liouville class #
The class is insensitive to changes of coefficient, value, and gradient representatives on null sets. The coefficient statement uses the unweighted characterization of the local symmetric Sobolev closure.
theorem
HCPolySupport.HighContrast.Root.memLiouvilleClass_congr_representatives
{d : ℕ}
{b : CoeffField d}
{theta : ℝ}
{u v : Vec d → ℝ}
{Du Dv : Vec d → Vec d}
(huv : u =ᵐ[MeasureTheory.volume] v)
(hDuDv : Du =ᵐ[MeasureTheory.volume] Dv)
:
Replacing the value and gradient representatives almost everywhere does not change membership in the Liouville class.
theorem
HCPolySupport.HighContrast.Root.memLiouvilleClass_congr_coefficient
{d : ℕ}
{a b : CoeffField d}
{theta : ℝ}
{v : Vec d → ℝ}
{Dv : Vec d → Vec d}
(hab : a =ᵐ[MeasureTheory.volume] b)
(ha : IsAELocallyUniformlyElliptic a)
(hb : IsAELocallyUniformlyElliptic b)
:
Almost-everywhere equal locally uniformly elliptic coefficient representatives define the same Liouville class.