Weak directional derivative

Definition

KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Basic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

HasWeakDerivAlong f g v means that $f$ and $g$ are locally integrable with respect to Lebesgue measure and that, for every $C^1$ compactly supported test function $\psi$ , $\int f(x)\,Df(x)[v]$ is replaced by the distributional identity $\int f(x)D\psi(x)[v]$ $=-\int g(x)\psi(x)\,dx$ . Thus g is the weak directional derivative of f along $v$ , with all integrability and test-function conditions explicit.

Original module imports

import FunctionalInequalities.Analysis.Mollification.Basic
import Mathlib

Original declaration excerpt

Shown in the original module context.

def HasWeakDerivAlong (f g : E → ℝ) (v : E) : Prop :=
  LocallyIntegrable f (volume : Measure E) ∧ LocallyIntegrable g (volume : Measure E) ∧
    ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ →
      ∫ x, f x * fderiv ℝ ψ x v ∂(volume : Measure E) = -∫ x, g x * ψ x ∂(volume : Measure E)

Module navigation

Direct project imports: Analysis/Mollification/Basic.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.WeakDerivative.Basic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic
import Mathlib

noncomputable section
open MeasureTheory
open scoped ContDiff
namespace FunctionalInequalities
namespace Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
/-- `g` is the **weak directional derivative** of `f` along `v`, tested against `C¹` functions with
compact support; both functions are locally integrable (so the integrals are not junk). Weak Letwin
route (routes/letwin-weak-definitions.md, item 4). -/
def HasWeakDerivAlong (f g : E → ℝ) (v : E) : Prop :=
  LocallyIntegrable f (volume : Measure E) ∧ LocallyIntegrable g (volume : Measure E) ∧
    ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ →
      ∫ x, f x * fderiv ℝ ψ x v ∂(volume : Measure E) = -∫ x, g x * ψ x ∂(volume : Measure E)
end Analysis
end FunctionalInequalities
universe u

Source

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

View graph