High-contrast homogenization: Analytic.CoefficientLocality

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The coefficient-weighted classes on a set read the field only on that set

The weighted energy sEnergyOn, the norm h1sNormSqOn of s.introduction, the skew-flux dual norm skewFluxDualNorm and the membership class MemH1a0 are built from integrals over the set V alone. Two coefficient fields agreeing almost everywhere on V therefore give the same weighted norm, the same skew-flux dual norm and the same membership class: none of them reads the field outside V.

This is what makes a locally uniformly elliptic field usable in the estimates stated for fields uniformly elliptic almost everywhere on all of ℝ^d. On a bounded domain the field agrees almost everywhere with such a field, and every class in the display is unchanged by the replacement.

theorem HCPolySupport.HighContrast.sEnergyOn_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (F : Vec d → Vec d) : sEnergyOn b V F = sEnergyOn b' V F

The weighted Dirichlet energy on V reads the field only on V.

theorem HCPolySupport.HighContrast.h1sNormSqOn_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (u : Vec d → ℝ) (Du : Vec d → Vec d) : h1sNormSqOn b V u Du = h1sNormSqOn b' V u Du

The H¹_s(V) norm square reads the field only on V.

theorem HCPolySupport.HighContrast.skewFluxPairing_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (F : Vec d → Vec d) (φ : Vec d → ℝ) : skewFluxPairing b V F φ = skewFluxPairing b' V F φ

The skew-flux pairing on V reads the field only on V: the two integrands agree almost everywhere there, so they are simultaneously absolutely convergent and have the same integral.

theorem HCPolySupport.HighContrast.skewFluxDualNorm_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (F : Vec d → Vec d) : skewFluxDualNorm b V F = skewFluxDualNorm b' V F

The skew-flux dual norm on V reads the field only on V: the test class and the pairing it takes the supremum of are both unchanged.

theorem HCPolySupport.HighContrast.memH1a_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (u : Vec d → ℝ) (Du : Vec d → Vec d) : MemH1a b V u Du ↔ MemH1a b' V u Du

Membership in H¹_a(V) reads the field only on V. Both clauses that see the coefficient field — the H¹_s approximation and the skew-flux dual approximation — are unchanged when the field is replaced by one agreeing with it almost everywhere on V.

theorem HCPolySupport.HighContrast.memH1a0_congr_coeff {d : ℕ} {b b' : CoeffField d} {V : Set (Vec d)} (h : b =ᵐ[MeasureTheory.volume.restrict V] b') (u : Vec d → ℝ) (Du : Vec d → Vec d) : MemH1a0 b V u Du ↔ MemH1a0 b' V u Du

Membership in H¹_{a,0}(V) reads the field only on V. Both clauses that see the coefficient field — the H¹_s approximation and the skew-flux dual approximation — are unchanged when the field is replaced by one agreeing with it almost everywhere on V.