Subtraction of weak multi-index derivatives

Proved

HunterPDE.Sobolev.HasWeakDeriv.sub

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

distributionssobolev-spacesweak-derivatives

If u is a weak multi-index derivative of f and v is the corresponding weak derivative of g on a domain, then u minus v is the weak derivative of f minus g. All four functions are locally integrable on the domain. No Lp or smoothness assumption on f and g is required.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open MeasureTheory HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.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

John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, printed pp. 47–48, Definitions 3.1–3.2 and uniqueness discussion; subtraction follows by linearity of the defining integrals.

View graph