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

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

Smooth-dual pairing with actual fractional Sobolev fields

This module closes the smooth-test dual pairing against an actual fractional Sobolev field which also has the required L² representative.

noncomputable def HCPolySupport.cubeEuclideanWspGraphPointOfField {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanWspField Q s p) : CubeEuclideanWspGraphAmbient Q p

The ambient full-norm graph point of an actual fractional field.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeEuclideanWspKernel_sub {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F G : Vec d → Vec d) : (cubeEuclideanWspKernel s p fun (x : Vec d) => F x - G x) = fun (z : Vec d × Vec d) => cubeEuclideanWspKernel s p F z - cubeEuclideanWspKernel s p G z

noncomputable def HCPolySupport.cubeEuclideanWspFieldSub {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F G : CubeEuclideanWspField Q s p) : CubeEuclideanWspField Q s p

Subtract fractional cube fields pointwise, retaining Euclidean L^p membership and L^p membership of the Gagliardo difference kernel.

Equations

• HCPolySupport.cubeEuclideanWspFieldSub F G = { toField := fun (x : HCPolySupport.Vec d) => F.toField x - G.toField x, euclideanMemLp := ⋯, euclideanMemWsp := ⋯ }

noncomputable def HCPolySupport.cubeEuclideanNormalizedFieldPairing {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (G : CubeEuclideanWspL2Field Q s p) : ℝ

The literal normalized-cube pairing of an L² field with an actual fractional Sobolev field.

Equations

• HCPolySupport.cubeEuclideanNormalizedFieldPairing F G = ∫ (x : HCPolySupport.Vec d), HCPolySupport.vecDot (F.toField x) (G.toField x) ∂HCPolySupport.normalizedCubeMeasure Q

theorem HCPolySupport.ennreal_ofReal_abs_cubeEuclideanNormalizedFieldPairing_le {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (G : CubeEuclideanWspL2Field Q s p.conjugate) : ENNReal.ofReal |cubeEuclideanNormalizedFieldPairing F G| ≤ cubeEuclideanNegativeWspSmoothDualENorm Q s p F * cubeEuclideanWspFullENorm Q s p.conjugate G.toField

The literal normalized-cube pairing is controlled by the smooth negative fractional-Sobolev dual norm.