Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspLpMembership #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-seminorm membership for Euclidean fractional Sobolev fields #
This file packages the product-measure measurability needed to turn a
normalized-cube L^p field with finite Euclidean fractional seminorm into a
literal MemCubeEuclideanWsp witness.
theorem
HCPolySupport.memCubeEuclideanWsp_of_memLp_of_eSeminorm_lt_top
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
{F : Vec d → Vec d}
(hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) p.exponent (normalizedCubeMeasure Q))
(hsemi : cubeEuclideanWspESeminorm Q s p F < ⊤)
:
MemCubeEuclideanWsp Q s p F
A normalized-cube Euclidean L^p field with finite fractional seminorm
belongs to the literal Euclidean fractional Sobolev membership predicate.