Weak-derivative test functions

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port separates the bundled test-function facade from the weak-derivative predicates and uses the CKN namespace.

structure CKN.WeakTestFunction {d : ℕ} (U : Set (Vec d)) : Type

A smooth compactly supported test function supported inside U.

• toFun : Vec d → ℝ

  Scalar test function used to express weak differentiation.

• contDiff : ContDiff ℝ (↑⊤) self.toFun
• hasCompactSupport : HasCompactSupport self.toFun
• tsupport_subset : tsupport self.toFun ⊆ U

@[instance_reducible]

instance CKN.instCoeFunWeakTestFunctionForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (WeakTestFunction U) fun (x : WeakTestFunction U) => Vec d → ℝ

Equations

• CKN.instCoeFunWeakTestFunctionForallVecReal = { coe := fun (φ : CKN.WeakTestFunction U) => φ.toFun }

noncomputable def CKN.WeakTestFunction.partialDeriv {d : ℕ} {U : Set (Vec d)} (φ : WeakTestFunction U) (i : Fin d) (x : Vec d) : ℝ

The classical ith derivative of a bundled test function.

Equations

• φ.partialDeriv i x = (fderiv ℝ φ.toFun x) (CKN.basisVec i)