Weak derivatives respect subtraction

Proved

HunterPDE.Shared.HasWeakDeriv.sub

by Mazecto · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationsobolev-spacesweak-derivatives

Let $\Omega\subset\mathbb R^n$ , let $\alpha$ be any multi-index, and suppose $u=\partial^\alpha f$ and $v=\partial^\alpha g$ weakly on $\Omega$ . Then

\partial^\alpha(f-g)=u-v.

Local integrability and the test identities are preserved under subtraction. No openness or Sobolev exponent is needed. This provides the linearity step for derivative convergence in the Shared weak-derivative interface.

Preamble

import Definitions.Def_HunterPDE_Shared_WeakDeriv
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp
import Mathlib.Analysis.Calculus.FDeriv.Const
import Mathlib.MeasureTheory.Integral.Bochner.Set

open MeasureTheory HunterPDE.Shared
open scoped ContDiff
set_option autoImplicit false

Formal statement

theorem HunterPDE.Shared.HasWeakDeriv.sub {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {α : Fin n → ℕ} {f g u v : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : HasWeakDeriv Ω α f u) (hv : HasWeakDeriv Ω α g v) :
    HasWeakDeriv Ω α (f - g) (u - v) := by sorry

Source

J. K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Theorems 3.42 and 3.44, printed pp. 72–73. Auxiliary ingredient for the normal Green identity, not an explicit numbered theorem in the source.

View graph