High-contrast homogenization: Provider.Regularity.CorrectorGlobalH1sLoc

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

Local weighted Sobolev membership of global corrector representatives

The global representatives of a projective local H¹ carrier agree on every exhaustion cube with an actual H1Function. Convex smooth approximation on a containing cube therefore supplies the ballwise approximation required by MemH1sLoc.

theorem HCPolySupport.HighContrast.exists_contDiff_tendsto_h1NormSqOnUnweighted_sub {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) : ∃ (w : ℕ → Vec d → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (w n)) ∧ Filter.Tendsto (fun (n : ℕ) => h1NormSqOnUnweighted U (fun (x : Vec d) => w n x - u.toFun x) fun (x : Vec d) => smoothGrad (w n) x - u.grad x) Filter.atTop (nhds 0)

Smooth convex approximation converges to an H1Function in the exact unweighted quantity used by the definition of MemH1sLoc.

theorem HCPolySupport.HighContrast.exists_closedBall_zero_subset_localGradientCube {d : ℕ} {R : ℝ} (hR : 0 < R) : ∃ (n : ℕ), Metric.closedBall 0 R ⊆ localGradientCube d n

theorem HCPolySupport.HighContrast.h1NormSqOnUnweighted_mono {d : ℕ} {V U : Set (Vec d)} (hVU : V ⊆ U) (u : Vec d → ℝ) (Du : Vec d → Vec d) : h1NormSqOnUnweighted V u Du ≤ h1NormSqOnUnweighted U u Du

theorem HCPolySupport.HighContrast.h1NormSqOnUnweighted_congr_ae {d : ℕ} {V : Set (Vec d)} {u v : Vec d → ℝ} {Du Dv : Vec d → Vec d} (hu : u =ᵐ[MeasureTheory.volume.restrict V] v) (hDu : Du =ᵐ[MeasureTheory.volume.restrict V] Dv) : h1NormSqOnUnweighted V u Du = h1NormSqOnUnweighted V v Dv