Almost-everywhere uniqueness of a weak multi-index derivative
ProvedHunterPDE.Sobolev.HasWeakDeriv.ae_eqdistributionssobolev-spacesweak-derivatives
On an open subset of Euclidean space, two locally integrable functions representing the same weak multi-index derivative of a function agree almost everywhere on that domain. This holds for every multi-index, including order zero, without an Lp hypothesis.
Preamble
import Definitions.Def_HunterPDE_Sobolev_SobolevSpace open MeasureTheory HunterPDE.Sobolev
Formal statement
theorem HunterPDE.Sobolev.HasWeakDeriv.ae_eq {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
(hΩ : IsOpen Ω) {α : Fin n → ℕ}
{f u v : EuclideanSpace ℝ (Fin n) → ℝ}
(hu : HasWeakDeriv Ω α f u) (hv : HasWeakDeriv Ω α f v) :
u =ᵐ[volume.restrict Ω] 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.