Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.FractionalDualToBesovBridge

High-contrast homogenization: Provider.PolynomialHomogenization.FractionalDualToBesovBridge #

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

Fractional dual to componentwise full Besov dual #

Below the trace threshold the physical negative fractional norm on a triadic cube is controlled by the sum of the scalar full Besov dual norms of its components, with a finite dimension-only coefficient. Both sides keep the physical cube scale.

source
noncomputable def HCPolySupport.HighContrast.fractionalDualToBesovConstant (d : ℕ) :
ENNReal

A finite dimension-only coefficient comparing the exact fractional smooth dual with the componentwise full Besov dual.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.fractionalDualToBesovConstant_lt_top (d : ℕ) :
    fractionalDualToBesovConstant d < ⊤
    source
    theorem HCPolySupport.HighContrast.negSobolevNorm_le_fractionalDualToBesovConstant_mul_fullDualSum {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F : CubeEuclideanLpField Q FiniteLpExponent.two) :
    negSobolevNorm (openCubeSet Q) s F.toField ≤ fractionalDualToBesovConstant d * ENNReal.ofReal (∑ i : Fin d, cubeBesovDualFullNorm Q s 2 2 fun (x : Vec d) => F.toField x i)

    Below the trace threshold, the physical negative fractional norm on a triadic cube is controlled by the sum of its scalar full Besov dual norms. Both sides retain the physical cube scale.