Locally Lipschitz functions are weakly differentiable

Let u : E → F be locally Lipschitz on an open subset Ω of a finite-dimensional real normed space E, and let μ be an additive Haar measure. If u has line derivative u' x in the direction v at almost every x ∈ Ω, then u' is the weak derivative of u in the direction v on Ω (LocallyLipschitzOn.hasWeakLineDerivOn). In the same way an almost-everywhere Fréchet derivative is the weak one (LocallyLipschitzOn.hasWeakFDerivOn), and when F is finite-dimensional, Rademacher's theorem supplies it: fderiv ℝ u is the weak derivative of u on Ω (LocallyLipschitzOn.hasWeakFDerivOn_fderiv). Near each point this weak derivative is bounded by a local Lipschitz constant (norm_fderiv_le_of_lipschitzOn).

No regularity of u beyond the local Lipschitz bound is used, and the codomain F is an arbitrary Banach space: the derivative is only assumed to exist almost everywhere. This is what a change of variables by a Lipschitz map, such as the flattening of the region above a Lipschitz graph, needs: composed with such a map, a smooth function is only locally Lipschitz.

The argument

For real u and a test function φ, u is Lipschitz on a compact neighbourhood of the support of φ inside Ω, so it agrees there with a globally Lipschitz function (LipschitzOnWith.extend_real). Mathlib's integration by parts for Lipschitz functions (LipschitzWith.integral_lineDeriv_mul_eq) applies to that extension, and near the support of φ its line derivative is u' almost everywhere. Measurability and local integrability of u' come from LocallyLipschitzOn.locallyIntegrableOn_of_ae_hasLineDerivAt. A vector-valued u is reduced to the real case by testing the identity against continuous linear functionals (TauCeti.hasWeakLineDerivOn_of_forall_strongDual).

Main declarations

• LocallyLipschitzOn.hasWeakLineDerivOn: an almost-everywhere line derivative of a locally Lipschitz function is its weak derivative.
• LocallyLipschitzOn.hasWeakFDerivOn: the same for an almost-everywhere Fréchet derivative.
• LocallyLipschitzOn.hasWeakFDerivOn_fderiv: for a finite-dimensional codomain, fderiv ℝ u is the weak derivative.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., §4.2.3, Theorem 4.5 and §3.1.2 (Rademacher's theorem).
• L. C. Evans, Partial Differential Equations, 2nd ed., §5.8.2, Theorem 4.

theorem LocallyLipschitzOn.hasWeakLineDerivOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {v : E} {u u' : E → F} [CompleteSpace F] (hu : LocallyLipschitzOn (↑Ω) u) (h : ∀ᵐ (x : E) ∂μ, x ∈ Ω → HasLineDerivAt ℝ u (u' x) x v) : TauCeti.HasWeakLineDerivOn μ Ω u u' v

A locally Lipschitz function is weakly differentiable. If u is locally Lipschitz on the open set Ω and has line derivative u' x in the direction v at almost every x ∈ Ω, then u' is the weak derivative of u in the direction v on Ω.

theorem LocallyLipschitzOn.hasWeakFDerivOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {u : E → F} [CompleteSpace F] {U : E → E →L[ℝ] F} (hu : LocallyLipschitzOn (↑Ω) u) (h : ∀ᵐ (x : E) ∂μ, x ∈ Ω → HasFDerivAt u (U x) x) : TauCeti.HasWeakFDerivOn μ Ω u U

A locally Lipschitz function is weakly differentiable. If u is locally Lipschitz on the open set Ω and has Fréchet derivative U x at almost every x ∈ Ω, then U is the weak derivative of u on Ω.

theorem LocallyLipschitzOn.hasWeakFDerivOn_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {u : E → F} [FiniteDimensional ℝ F] (hu : LocallyLipschitzOn (↑Ω) u) : TauCeti.HasWeakFDerivOn μ Ω u (fderiv ℝ u)

A locally Lipschitz function has its derivative as weak derivative. A function between finite-dimensional real normed spaces that is locally Lipschitz on the open set Ω has fderiv ℝ u as its weak derivative on Ω; by Rademacher's theorem it is differentiable almost everywhere there.