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

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

Descendant localization preliminaries for the smooth negative fractional norm

This module records the exact normalized-pairing partition and the canonical restriction of a globally smooth test field. They are the two analytic inputs needed for negative-norm localization by finite Hoelder duality.

def HCPolySupport.CubeEuclideanWspSmoothTest.restrictToSubcube {d : ℕ} {Q R : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) (_hRQ : openCubeSet R ⊆ openCubeSet Q) : CubeEuclideanWspSmoothTest R s p

The same globally smooth test field viewed on a subcube.

Equations

• h.restrictToSubcube _hRQ = { toField := h.toField, contDiff := ⋯ }

def HCPolySupport.CubeEuclideanWspSmoothTest.scale {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (c : ℝ) (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspSmoothTest Q s p

The smooth fractional Sobolev test obtained by multiplying its vector field by the real scalar c.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.scale c h = { toField := fun (x : HCPolySupport.Vec d) => c • h.toField x, contDiff := ⋯ }

theorem HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm_le_descendantsENNAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeWspSmoothDualENorm Q s p F ≤ ENNReal.ofReal 3 ^ (↑j * ↑s) * (descendantsENNAverage Q j fun (R : TriadicCube d) => if hR : R ∈ descendantsAtDepth Q j then cubeEuclideanNegativeWspSmoothDualENorm R s p (F.restrictToSubcube ⋯) ^ p.exponent.toReal else 0) ^ p.exponent.toReal⁻¹

The smooth negative full dual norm localizes over triadic descendants with the exact normalized outer ℓᵖ average.