Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapFinitePGlobalBound

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

noncomputable def HCPolySupport.exactOverlapDepthGlobalBoundConstant (d : ℕ) : ENNReal

A finite dimension-only constant for the global bound on one exact-overlap depth energy.

Equations

• HCPolySupport.exactOverlapDepthGlobalBoundConstant d = 2 * 3 ^ d

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_le_global {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) p.exponent (normalizedCubeMeasure Q)) : cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ≤ exactOverlapDepthGlobalBoundConstant d * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (F x)) p.exponent (normalizedCubeMeasure Q)

At each retained depth, exact Euclidean overlap oscillation is bounded by a finite dimension-only multiple of the parent normalized L^p norm.