Classical first partial derivatives are weak derivatives on an open set

Proved

HunterPDE.Shared.hasWeakDeriv_partial_of_contDiffOn

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

integration-by-partspdeweak-derivatives

Let Ω be an open subset of Euclidean space and let f be continuously differentiable on Ω. For every coordinate i, the classical partial derivative ∂ᵢf is a weak first derivative on Ω. Both functions are locally integrable there, and integration by parts holds against every smooth test function with compact support contained in Ω. No assumptions on f outside Ω, boundary regularity, or compact support of f are required.

Preamble

import Definitions.Def_HunterPDE_Shared_WeakDeriv
import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
import Mathlib.Analysis.Calculus.ContDiff.Comp
import Mathlib.MeasureTheory.Integral.Bochner.Set

open MeasureTheory HunterPDE.Shared
open scoped ContDiff
set_option autoImplicit false

Formal statement

theorem HunterPDE.Shared.hasWeakDeriv_partial_of_contDiffOn {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    (hΩ : IsOpen Ω) (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ContDiffOn ℝ 1 f Ω) (i : Fin n) :
    HasWeakDeriv Ω (Pi.single i 1) f (partialDeriv f i) := by sorry

Source

J. K. Hunter, Notes on Partial Differential Equations, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Definitions 3.1–3.2 and discussion on printed pp. 47–48: continuously differentiable functions have their classical derivatives as weak derivatives. The C¹ open-set case is proved by integration by parts against compactly supported tests.

View graph