Weak first derivatives on native vector domains

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port preserves the raw integration-by-parts predicates, a.e. uniqueness, restriction, and smooth-function constructors, while using the CKN namespace and the reduced weak-derivative dependency surface.

def CKN.HasWeakPartialDerivOn {d : ℕ} (U : Set (Vec d)) (i : Fin d) (u gi : Vec d → ℝ) : Prop

gi is the ith weak derivative of u on U.

Equations

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

def CKN.HasWeakGradientOn {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : Prop

Du is a coordinate weak gradient of u on U.

Equations

• CKN.HasWeakGradientOn U u Du = ∀ (i : Fin d), CKN.HasWeakPartialDerivOn U i u fun (x : CKN.Vec d) => Du x i

theorem CKN.hasWeakPartialDerivOn_iff_forall_testFunction {d : ℕ} {U : Set (Vec d)} {i : Fin d} {u gi : Vec d → ℝ} : HasWeakPartialDerivOn U i u gi ↔ ∀ (φ : WeakTestFunction U), ∫ (x : Vec d) in U, u x * φ.partialDeriv i x = -∫ (x : Vec d) in U, gi x * φ.toFun x

theorem CKN.HasWeakPartialDerivOn.ae_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {i : Fin d} {u gi hi : Vec d → ℝ} (hgiLoc : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume) (hhiLoc : MeasureTheory.LocallyIntegrableOn hi U MeasureTheory.volume) (hgi : HasWeakPartialDerivOn U i u gi) (hhi : HasWeakPartialDerivOn U i u hi) : gi =ᵐ[volumeOn U] hi

Locally integrable weak partial derivatives are unique almost everywhere.

theorem CKN.HasWeakPartialDerivOn.restrict {d : ℕ} {U V : Set (Vec d)} : IsOpen V → ∀ (hVU : V ⊆ U) {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi), HasWeakPartialDerivOn V i u gi

theorem CKN.HasWeakGradientOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVOpen : IsOpen V) (hVU : V ⊆ U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du

theorem CKN.HasWeakPartialDerivOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {i : Fin d} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakPartialDerivOn U i f fun (x : Vec d) => (fderiv ℝ f x) (basisVec i)

theorem CKN.HasWeakGradientOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakGradientOn U f fun (x : Vec d) (i : Fin d) => (fderiv ℝ f x) (basisVec i)