Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspSmoothDensity #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Smooth density for Euclidean fractional Sobolev fields #
This module is the source-facing smooth-density layer for the Euclidean fractional full norm on a triadic cube.
noncomputable def
HCPolySupport.cubeEuclideanWspConvexApproxSmoothField
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(F : CubeEuclideanWspField Q s p)
(x0 : Vec d)
(r ε : ℝ)
:
The global componentwise convex smoothing representative of a Euclidean fractional field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.contDiff_cubeEuclideanWspConvexApproxSmoothField
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(F : CubeEuclideanWspField Q s p)
(x0 : Vec d)
{r ε : ℝ}
(hr : 0 < r)
(hε : 0 < ε)
:
ContDiff ℝ (↑⊤) (cubeEuclideanWspConvexApproxSmoothField F x0 r ε)
noncomputable def
HCPolySupport.cubeEuclideanWspConvexApproxSmoothTest
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(F : CubeEuclideanWspField Q s p)
(x0 : Vec d)
{r ε : ℝ}
(hr : 0 < r)
(hε : 0 < ε)
:
Package coordinatewise convex smoothing with positive radius and smoothing scale as a smooth test field for the fractional cube space.
Equations
- HCPolySupport.cubeEuclideanWspConvexApproxSmoothTest F x0 hr hε = { toField := HCPolySupport.cubeEuclideanWspConvexApproxSmoothField F x0 r ε, contDiff := ⋯ }
Instances For
theorem
HCPolySupport.exists_cubeEuclideanWspSmoothTest_fullENorm_and_l2_sub_lt
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{q : FiniteLpExponent}
(G : CubeEuclideanWspL2Field Q s q)
{epsilon : ENNReal}
(hepsilon : 0 < epsilon)
:
∃ (h : CubeEuclideanWspSmoothTest Q s q),
(cubeEuclideanWspFullENorm Q s q fun (x : Vec d) => h.toField x - G.toField x) < epsilon ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (h.toField x - G.toField x)) 2
(normalizedCubeMeasure Q) < epsilon
A single explicit convex smoothing approximant is simultaneously close in
the full fractional norm and in normalized L².
theorem
HCPolySupport.exists_cubeEuclideanWspSmoothTest_fullENorm_sub_lt
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(F : CubeEuclideanWspField Q s p)
{epsilon : ENNReal}
(hepsilon : 0 < epsilon)
:
∃ (h : CubeEuclideanWspSmoothTest Q s p),
(cubeEuclideanWspFullENorm Q s p fun (x : Vec d) => h.toField x - F.toField x) < epsilon