Coarse-graining support: Support.Sobolev.SmoothCompactSupport

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

Smooth compactly supported test functions

This is a thin adapter over Mathlib's genuine test-function carrier 𝓓^{⊤}(Ω, ℝ). It records the concrete Euclidean-coordinate gradient used by the project's weak Sobolev witnesses, without introducing a second test-space structure or any regularity hypothesis on Ω.

@[reducible, inline]

abbrev HCPolySupport.SmoothCompactSupportFunction {d : ℕ} (Ω : TopologicalSpace.Opens (Vec d)) : Type

Mathlib's smooth compactly supported real-valued test functions on Ω.

Equations

• HCPolySupport.SmoothCompactSupportFunction Ω = TestFunction Ω ℝ ⊤

noncomputable def HCPolySupport.SmoothCompactSupportFunction.gradient {d : ℕ} {Ω : TopologicalSpace.Opens (Vec d)} (φ : SmoothCompactSupportFunction Ω) : Vec d → Vec d

The explicit Euclidean-coordinate gradient of a smooth test function.

Equations

• φ.gradient x i = (fderiv ℝ (⇑φ) x) (HCPolySupport.basisVec i)

theorem HCPolySupport.SmoothCompactSupportFunction.contDiff {d : ℕ} {Ω : TopologicalSpace.Opens (Vec d)} (φ : SmoothCompactSupportFunction Ω) : ContDiff ℝ ↑⊤ ⇑φ

The literal global smoothness fact carried by Mathlib's test-function type.

theorem HCPolySupport.SmoothCompactSupportFunction.hasCompactSupport {d : ℕ} {Ω : TopologicalSpace.Opens (Vec d)} (φ : SmoothCompactSupportFunction Ω) : HasCompactSupport ⇑φ

The literal compact-support fact carried by Mathlib's test-function type.

theorem HCPolySupport.SmoothCompactSupportFunction.tsupport_subset {d : ℕ} {Ω : TopologicalSpace.Opens (Vec d)} (φ : SmoothCompactSupportFunction Ω) : tsupport ⇑φ ⊆ ↑Ω

The literal support-in-domain fact carried by Mathlib's test-function type.

noncomputable def HCPolySupport.SmoothCompactSupportFunction.toW1pFunction {d : ℕ} (Ω : TopologicalSpace.Opens (Vec d)) (p : ENNReal) (φ : SmoothCompactSupportFunction Ω) : W1pFunction (↑Ω) p

Regard a smooth compactly supported test function as a W^{1,p} function on its open support domain.

Equations

• HCPolySupport.SmoothCompactSupportFunction.toW1pFunction Ω p φ = HCPolySupport.W1pFunction.ofContDiff ⋯ ⋯ ⋯ p

@[simp]

theorem HCPolySupport.SmoothCompactSupportFunction.toW1pFunction_toFun {d : ℕ} (Ω : TopologicalSpace.Opens (Vec d)) (p : ENNReal) (φ : SmoothCompactSupportFunction Ω) : (toW1pFunction Ω p φ).toFun = ⇑φ

@[simp]

theorem HCPolySupport.SmoothCompactSupportFunction.toW1pFunction_grad {d : ℕ} (Ω : TopologicalSpace.Opens (Vec d)) (p : ENNReal) (φ : SmoothCompactSupportFunction Ω) : (toW1pFunction Ω p φ).grad = φ.gradient

@[simp]

theorem HCPolySupport.SmoothCompactSupportFunction.gradient_neg {d : ℕ} {Ω : TopologicalSpace.Opens (Vec d)} (φ : SmoothCompactSupportFunction Ω) : (-φ).gradient = -φ.gradient

Negating a test function negates its explicit gradient. This is the sign compatibility needed when symmetric test classes are used in dual suprema.