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

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

Algebraic carrier for smooth Euclidean fractional-Sobolev tests

This module supplies the pointwise real vector-space structure on globally smooth test fields. The subsequent completed-dual graph will map this carrier to two L^p components once the separate diagonal-singularity integrability lemma establishes that every smooth test has finite Gagliardo seminorm.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.ext {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {h k : CubeEuclideanWspSmoothTest Q s p} (hfield : h.toField = k.toField) : h = k

Smooth test fields are determined by their pointwise vector fields.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.ext_iff {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {h k : CubeEuclideanWspSmoothTest Q s p} : h = k ↔ h.toField = k.toField

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instZero {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : Zero (CubeEuclideanWspSmoothTest Q s p)

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instZero = { zero := { toField := 0, contDiff := ⋯ } }

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instAdd {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : Add (CubeEuclideanWspSmoothTest Q s p)

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instAdd = { add := fun (h k : HCPolySupport.CubeEuclideanWspSmoothTest Q s p) => { toField := h.toField + k.toField, contDiff := ⋯ } }

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instNeg {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : Neg (CubeEuclideanWspSmoothTest Q s p)

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instNeg = { neg := fun (h : HCPolySupport.CubeEuclideanWspSmoothTest Q s p) => { toField := -h.toField, contDiff := ⋯ } }

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instSub {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : Sub (CubeEuclideanWspSmoothTest Q s p)

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instSub = { sub := fun (h k : HCPolySupport.CubeEuclideanWspSmoothTest Q s p) => h + -k }

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instAddCommGroup {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : AddCommGroup (CubeEuclideanWspSmoothTest Q s p)

Equations

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

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instSMulReal {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : SMul ℝ (CubeEuclideanWspSmoothTest Q s p)

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.instSMulReal = { smul := fun (c : ℝ) (h : HCPolySupport.CubeEuclideanWspSmoothTest Q s p) => { toField := c • h.toField, contDiff := ⋯ } }

@[instance_reducible]

instance HCPolySupport.CubeEuclideanWspSmoothTest.instModuleReal {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : Module ℝ (CubeEuclideanWspSmoothTest Q s p)

Equations

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

@[simp]

theorem HCPolySupport.CubeEuclideanWspSmoothTest.toField_zero {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : toField 0 = 0

@[simp]

theorem HCPolySupport.CubeEuclideanWspSmoothTest.toField_add {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h k : CubeEuclideanWspSmoothTest Q s p) : (h + k).toField = h.toField + k.toField

@[simp]

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

@[simp]

theorem HCPolySupport.CubeEuclideanWspSmoothTest.toField_smul {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (c : ℝ) (h : CubeEuclideanWspSmoothTest Q s p) : (c • h).toField = c • h.toField

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.toCubeEuclideanWspField {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspField Q s p

The exact fractional-Sobolev field represented by a smooth test.

This is the source-facing graph map: it changes neither the pointwise field nor either constituent of the approved full W^(s,p) norm. Completion and dual identification remain deliberately outside this module.

Equations

• h.toCubeEuclideanWspField = { toField := h.toField, euclideanMemLp := ⋯, euclideanMemWsp := ⋯ }

@[simp]

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

theorem HCPolySupport.CubeEuclideanWspSmoothTest.toCubeEuclideanWspField_eSeminorm_eq {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : cubeEuclideanWspESeminorm Q s p h.toCubeEuclideanWspField.toField = cubeEuclideanWspESeminorm Q s p h.toField

The graph representative has exactly the original Gagliardo seminorm.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.toCubeEuclideanWspField_fullENorm_eq {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : cubeEuclideanWspFullENorm Q s p h.toCubeEuclideanWspField.toField = cubeEuclideanWspFullENorm Q s p h.toField

The graph representative has exactly the approved full W^(s,p) norm.