Weak derivatives and tempered distributions #
For an Lᵖ function and an L^q candidate derivative, with 1 ≤ p, q ≤ ∞, the weak
directional derivative identity on the whole space is equivalent to equality of their tempered
distributions after differentiation. The
weak derivative is tested against real compactly supported functions; the tempered derivative
is tested against complex Schwartz functions. Both notions therefore give the same derivative,
without a smoothness or compact-support assumption on the Lᵖ functions.
This is the derivative bridge between domain Sobolev spaces and the Fourier description of whole-space Sobolev spaces. The measure may be any locally finite measure of temperate growth; the forward implication only requires temperate growth.
References #
- L. C. Evans, Partial Differential Equations, Section 5.2 (weak derivatives).
- L. Hörmander, The Analysis of Linear Partial Differential Operators I, Section 7.1.
The formalization uses Mathlib's MeasureTheory.Lp.toTemperedDistribution and the real-test
extensionality theorem TauCeti.temperedDistribution_ext_real.
Differentiating an Lᵖ function as a tempered distribution gives its weak directional
derivative whenever that derivative is represented by an L^q function, q ≥ 1.
If the tempered derivative of an Lᵖ function is represented by another Lᵖ function,
possibly with a different exponent, then the latter is its weak directional derivative on the
whole space.
For an Lᵖ function and an L^q candidate derivative, 1 ≤ p, q ≤ ∞, weak differentiation
on the whole space is exactly
differentiation of the associated tempered distributions.
A real-valued Lᵖ function has weak derivative u' exactly when the complexified
tempered distributions satisfy the derivative equation. This form applies to real Sobolev
functions using Mathlib's complex Fourier transform.