Classical Derivatives Give Weak Directional Derivatives

Proved

FunctionalInequalities.Analysis.hasWeakDerivAlong_of_contDiff_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the identification of classical and weak directional derivatives.

Let $E$ be a finite-dimensional real inner-product space with measurable and Borel structures, let $f:E\to\mathbb R$ be $C^1$ , and fix $v\in E$ . Then fderiv ℝ f x v is a weak derivative of $f$ along $v$ :

D_v^{\mathrm{weak}}f(x)=Df(x)v.

In Lean this is expressed as HasWeakDerivAlong f (fun x => fderiv ℝ f x v) v. The result includes the local integrability conditions required by the weak derivative interface.

Original Lean declaration header

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

theorem hasWeakDerivAlong_of_contDiff {f : E → ℝ} (hf : ContDiff ℝ 1 f) (v : E) :
    HasWeakDerivAlong f (fun x => fderiv ℝ f x v) v

Module navigation

Module: Analysis/WeakDerivative/Basic.

Next: hasWeakDerivAlong_of_lipschitz.

Source excerpt, lines 43–44 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Basic

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.hasWeakDerivAlong_of_contDiff_readable {f : E → ℝ} (hf : ContDiff ℝ 1 f) (v : E) :
    HasWeakDerivAlong f (fun x => fderiv ℝ f x v) v := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/WeakDerivative/Basic.lean#L41-L68 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.WeakDerivative.Basic`, declaration `FunctionalInequalities.Analysis.hasWeakDerivAlong_of_contDiff`; the repository is private at upload time).

View graph