High-contrast homogenization: Provider.PolynomialHomogenization.CompactTestDensity

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

Compactly supported fractional test fields

Smooth vector fields compactly supported in an open triadic cube are dense in the normalized fractional square norm below order one half.

theorem HCPolySupport.HighContrast.exists_localVecTest_hsNormSq_sub_lt_smooth_of_lt_half {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (h : Vec d → Vec d) (hsmooth : ContDiff ℝ (↑⊤) h) {epsilon : ENNReal} (hepsilon : 0 < epsilon) : ∃ (psi : Vec d → Vec d), IsLocalVecTest (openCubeSet Q) psi ∧ (hsNormSq (openCubeSet Q) s fun (x : Vec d) => psi x - h x) < epsilon

A globally smooth field on a cube can be approximated in the normalized fractional square norm by globally smooth fields compactly supported in the open cube whenever the fractional order is below one half.