High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.FiniteNegSobolevPrice

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

theorem HCPolySupport.HighContrast.negSobolevNorm_le_inverseWeight_normalizedDual {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F : Vec d → Vec d) (hF : MemVectorL2 (cubeSet Q) F) : negSobolevNorm (openCubeSet Q) s F ≤ fractionalDualToBesovConstant d * ENNReal.ofReal ((cubeBesovScaleWeight s Q)⁻¹ * cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s F)

The physical compact-test fractional dual is the inverse cube weight times the response theorem's scale-normalized full dual, up to the available finite dimension constant.

theorem HCPolySupport.HighContrast.inverse_originCubeBesovWeight {d : ℕ} (s : ℝ) (m : ℤ) : (cubeBesovScaleWeight s (originCube d m))⁻¹ = Real.rpow 3 (s * ↑m)

On an origin cube, removing the normalizing Besov weight costs exactly the physical factor 3^(s*m).