Weak Directional Derivative of a Lipschitz Function

This is a weak-derivative form of the almost-everywhere differentiability theorem for Lipschitz functions.

Let $E$ be a finite-dimensional real inner-product space, let $f:E\to\mathbb R$, and let $L\in[0,\infty)$ be a Lipschitz constant. If $f$ is $L$-Lipschitz, then for every direction $v\in E$, the function

with fderiv interpreted pointwise is a weak derivative of $f$ in direction $v$. Equivalently, it satisfies the weak directional integration-by-parts identity against the test functions occurring in HasWeakDerivAlong.

The result provides the weak derivative interface needed to use Rademacher derivatives in integration-by-parts arguments.

Formalization Note. The conclusion is the predicate HasWeakDerivAlong; the derivative is the pointwise Fréchet derivative, and the identification is understood in the almost-everywhere sense with respect to volume measure.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem hasWeakDerivAlong_of_lipschitz {f : E → ℝ} {L : NNReal} (hf : LipschitzWith L f) (v : E) :
    HasWeakDerivAlong f (fun x => fderiv ℝ f x v) v

Module navigation

Module: Analysis/WeakDerivative/Basic.

Previous: hasWeakDerivAlong_of_contDiff · Next: HasWeakDerivAlong.mul_contDiff.

Source excerpt, lines 71–72 · Frozen source 408915f.