Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingDescendantWsp #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Descendant localization of the source fractional-Sobolev carrier #
The source finite-p datum is available on the parent cube. This file
provides its literal restriction to every triadic descendant, so one-cube
estimates can construct their regularity witnesses locally without adding a
new hypothesis to the local coarse-graining theorem.
theorem
HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp.onDescendant
{d : ℕ}
{Q R : TriadicCube d}
{n : ℤ}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
{g : Vec d → Vec d}
(hn : n ≤ Q.scale)
(hR : R ∈ descendantsAtScale Q n)
(hg : MemCubeEuclideanFullWsp Q s p g)
:
MemCubeEuclideanFullWsp R s p g
A parent full Euclidean W^{s,p} source witness restricts canonically to
every triadic descendant.