The zeroth weak derivative equals the original function almost everywhere

Proved

HunterPDE.Sobolev.HasWeakDeriv.zero_ae_eq

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

sobolev-spacesweak-derivatives

Let $\Omega\subseteq\mathbb R^n$ be open. If $g$ is the weak derivative of $f$ for the zero multi-index, then $g=f$ almost everywhere in $\Omega$ . The functions are locally integrable by the definition of a weak derivative. This identifies the zeroth term in the Sobolev norm with the ordinary $L^p$ norm.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open MeasureTheory HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.HasWeakDeriv.zero_ae_eq {n : ℕ}
    {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : IsOpen Ω)
    {f g : EuclideanSpace ℝ (Fin n) → ℝ}
    (hg : HasWeakDeriv Ω (fun _ => 0) f g) :
    g =ᵐ[volume.restrict Ω] f := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, p. 48, Definition 3.2 with the zero multi-index; p. 58, Definition 3.23

View graph