Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorGlobalAffineH1sLoc

High-contrast homogenization: Provider.Regularity.CorrectorGlobalAffineH1sLoc #

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

Local Sobolev membership of affine-plus-corrector representatives #

The global shell representatives agree on every exhaustion cube with the canonical local carrier. Adding the prescribed affine function and an arbitrary constant therefore preserves the ballwise H¹_s construction.

source
theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memH1sLoc_affineAdd_globalRepresentatives {d : ℕ} (z : NormalizedLocalH1Carrier d) {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (e : Vec d) (c : ℝ) :
MemH1sLoc b (fun (x : Vec d) => vecDot e x + z.globalValueRepresentative x + c) fun (x : Vec d) => e + z.globalGradientRepresentative x

The affine-plus-global-corrector pair, with an arbitrary additive constant, belongs to H¹_{s,loc}.