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

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

Smooth full-dual surface for Euclidean fractional Sobolev fields

The smooth-test supremum is retained as a SmoothDualENorm; no completion or density assertion is made in this module.

structure HCPolySupport.CubeEuclideanWspSmoothTest {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : Type

A globally smooth vector field used to test the full normalized fractional Sobolev norm on a cube.

• toField : Vec d → Vec d

  The underlying globally defined vector field.

• contDiff : ContDiff ℝ (↑⊤) self.toField

  Global C∞ regularity of the test field.

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instCoeFunForallVec {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : CoeFun (CubeEuclideanWspSmoothTest Q s p) fun (x : CubeEuclideanWspSmoothTest Q s p) => Vec d → Vec d

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instCoeFunForallVec = { coe := fun (h : HCPolySupport.CubeEuclideanWspSmoothTest Q s p) => h.toField }

theorem HCPolySupport.CubeEuclideanWspSmoothTest.euclideanMemLp_of_continuous {d : ℕ} (Q : TriadicCube d) (q : ENNReal) {f : Vec d → Vec d} (hf : Continuous f) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (f x)) q (normalizedCubeMeasure Q)

A globally continuous vector field has finite Euclidean L^q norm on a normalized cube for every exponent.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.euclideanMemLp_two {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h.toField x)) 2 (normalizedCubeMeasure Q)

A globally smooth test automatically supplies the Euclidean L² certificate needed for pairing with the represented L² field.

@[reducible, inline]

abbrev HCPolySupport.CubeEuclideanWspSmoothUnitTest {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : Type

A smooth test field in the unit ball of the full normalized fractional Sobolev power norm.

Equations

• HCPolySupport.CubeEuclideanWspSmoothUnitTest Q s p = { h : HCPolySupport.CubeEuclideanWspSmoothTest Q s p // HCPolySupport.cubeEuclideanWspFullENorm Q s p h.toField ≤ 1 }

noncomputable def HCPolySupport.cubeEuclideanNormalizedSmoothPairing {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (h : CubeEuclideanWspSmoothTest Q s p) : ℝ

The volume-normalized L² pairing of a represented field with a smooth fractional Sobolev test field.

Equations

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

def HCPolySupport.CubeEuclideanWspSmoothTest.smul {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (c : ℝ) (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspSmoothTest Q s p

The smooth fractional Sobolev test obtained by multiplying its vector field by the real scalar c.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.smul c h = { toField := fun (x : HCPolySupport.Vec d) => c • h.toField x, contDiff := ⋯ }

theorem HCPolySupport.cubeEuclideanNormalizedSmoothPairing_integrable {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (h : CubeEuclideanWspSmoothTest Q s p) : MeasureTheory.Integrable (fun (x : Vec d) => vecDot (F.toField x) (h.toField x)) (normalizedCubeMeasure Q)

noncomputable def HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : ENNReal

The extended norm obtained by taking the supremum of normalized pairings over the smooth unit ball in the conjugate full fractional Sobolev norm.

Equations

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

def HCPolySupport.CubeEuclideanSmoothPairingIsBounded {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : Prop

The normalized pairing is bounded by the conjugate full fractional Sobolev power norm on every globally smooth test field.

Equations

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

theorem HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm_lt_top_iff {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeWspSmoothDualENorm Q s p F < ⊤ ↔ CubeEuclideanSmoothPairingIsBounded Q s p F