Classical derivatives of smooth functions are weak derivatives

Proved

HunterPDE.Sobolev.hasWeakDeriv_of_contDiff

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

real-analysissobolev-spacesweak-derivatives

Let $u:\mathbb R^n\to\mathbb R$ be smooth and let $\alpha\in\mathbb N_0^n$ be a multi-index. Its classical derivative is also its weak derivative on the whole space:

\int_{\mathbb R^n}D^\alpha u\,\psi\,dx =(-1)^{|\alpha|}\int_{\mathbb R^n}u\,D^\alpha\psi\,dx \qquad(\psi\in C_c^\infty(\mathbb R^n)).

Both $u$ and its classical derivative are locally integrable. No compact support or global integrability assumption on $u$ is imposed. This identifies classical and weak derivatives of smooth functions for Sobolev and distribution arguments, including order zero and dimension zero.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
open MeasureTheory HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.hasWeakDeriv_of_contDiff {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℝ)
    (hu : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) u) (α : Fin n → ℕ) :
    HasWeakDeriv Set.univ α u (iteratedPartial α u) := 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, Section 1.8 (p. 10), Definitions 3.1–3.2 (pp. 47–48). Supporting calculus result: repeated integration by parts and support locality of derivatives.

View graph