Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.EuclideanWspExactOverlapFullControl

Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspExactOverlapFullControl #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Full exact-overlap control for Euclidean fractional-Sobolev fields #

This module adds the inhomogeneous scalar-coordinate estimate needed to use smooth Euclidean fractional-Sobolev fields as positive exact-overlap tests. The constant is chosen before the cube, fractional order, exponent, field, and coordinate.

source
noncomputable def HCPolySupport.cubeEuclideanWspExactOverlapFullControlConstant (d : ℕ) :
ENNReal

A dimension-only full positive-test constant.

Equations
Instances For
    source
    theorem HCPolySupport.cubeEuclideanWspExactOverlapFullControlConstant_lt_top (d : ℕ) :
    cubeEuclideanWspExactOverlapFullControlConstant d < ⊤
    source
    theorem HCPolySupport.exactOverlapIntegrableOfEuclideanWspField {d : ℕ} {s : ↑FractionalOrder} (Q : TriadicCube d) (p : FiniteLpExponent) (F : CubeEuclideanWspField Q s p) (i : Fin d) :
    ExactOverlapIntegrable Q fun (x : Vec d) => F.toField x i
    source
    theorem HCPolySupport.exactOverlapScalarPFullNorm_le_dimensionConstant_mul_cubeEuclideanWspFull {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanWspField Q s p) (i : Fin d) :
    exactOverlapFiniteNorm (exactOverlapScalarPParameters s p) Q (fun (x : Vec d) => F.toField x i) ⋯ ≤ cubeEuclideanWspExactOverlapFullControlConstant d * cubeEuclideanWspFullENorm Q s p F.toField

    Each scalar coordinate exact-overlap full norm is bounded by one explicit dimension-only multiple of the Euclidean fractional-Sobolev full norm. The coordinate's root and overlap integrability certificates are derived from the Euclidean L^p carrier.