Coarse-graining support: Support.Book.Ch03.ABK26.FinitePToLegacyQTwo #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Strict finite-p to legacy q = 2 Besov regularity #
This adapter transports the source finite-p carrier to the legacy signed
H^s right-hand-side carrier consumed by the one-cube deterministic theorem.
The quantitative strict-gap summation is owned by
LocalCoarseGrainingForcing.
theorem
HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp.toCubeVectorBesovHRegularity_neg_of_lt
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{s s2 : ↑FractionalOrder}
{p : FiniteLpExponent}
{g : Vec d → Vec d}
(hg : MemCubeEuclideanFullWsp Q s2 p g)
(hp : 2 ≤ p.exponent)
(hss2 : ↑s < ↑s2)
:
CubeVectorBesovHRegularity Q ↑s fun (x : Vec d) => -g x
A strict finite-p Euclidean fractional-Sobolev witness supplies the
legacy H^s right-hand-side carrier. The output sign is the one used by the
weak forced-equation interface.