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

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

Fractional Sobolev membership of smooth cube tests

The only analytic input in this file is the local integrability of a radial power kernel with positive gain over the dimension. It is then applied to the Lipschitz bound supplied by global smoothness on the bounded cube.

noncomputable def HCPolySupport.smoothWspPowerKernel {d : ℕ} (a : ℝ) (x y : Vec d) : ℝ

The power kernel ‖x - y‖^(a - d) for the ambient coordinate norm.

Equations

• HCPolySupport.smoothWspPowerKernel a x y = ‖x - y‖ ^ (a - ↑d)

noncomputable def HCPolySupport.smoothWspLpMajorant {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) : Vec d × Vec d → ℝ

The ambient-distance power ‖x - y‖^(1 - s - d/p) used to majorize a smooth fractional difference kernel up to a constant.

Equations

• HCPolySupport.smoothWspLpMajorant s p z = ‖z.1 - z.2‖ ^ (1 - ↑s - ↑d / p.exponent.toReal)

theorem HCPolySupport.CubeEuclideanWspSmoothTest.memCubeEuclideanWsp {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : MemCubeEuclideanWsp Q s p h.toField

A globally smooth vector field has finite cube fractional-Sobolev seminorm.

The positive-dimensional proof controls the off-diagonal kernel by a Lipschitz majorant; in dimension zero the target vector space is subsingleton, so the kernel vanishes identically.