Weak Derivative of a Negative Exponential

Proved

FunctionalInequalities.Analysis.hasWeakDerivAlong_exp_neg_of_lipschitz_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

Let $E$ be a finite-dimensional real inner-product space with Borel structure, let $F:E\to\mathbb{R}$ be globally $L$ -Lipschitz, and fix a direction $v\in E$ . Then $e^{-F}$ has weak derivative along $v$ given by

\partial_v(e^{-F})(x)=-e^{-F(x)}\,Df(x)[v],

where $Df$ is represented by fderiv. Moreover, the derivative density belongs to $L^2$ on the restriction of Lebesgue measure to every compact set. No boundedness of $F$ or global integrability of $e^{-F}$ is required.

Original Lean declaration header

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

theorem hasWeakDerivAlong_exp_neg_of_lipschitz {E : Type u}
    [instNormedAddCommGroup : NormedAddCommGroup E]
    [instInnerProductSpace : InnerProductSpace ℝ E]
    [instFiniteDimensional : FiniteDimensional ℝ E]
    [instMeasurableSpace : MeasurableSpace E] [instBorelSpace : BorelSpace E]
    {F : E → ℝ} {L : NNReal} (hF : LipschitzWith L F) (v : E) :
    HasWeakDerivAlong (fun x => Real.exp (-F x))
      (fun x => -Real.exp (-F x) * fderiv ℝ F x v) v ∧
    ∀ S : Set E, IsCompact S →
      MemLp (fun x => -Real.exp (-F x) * fderiv ℝ F x v) 2
        ((volume : Measure E).restrict S)

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: hasWeakDerivAlong_of_lipschitz.

Previous: hasWeakDerivAlong_finsetProd_of_locally_memLp_two · Next: HasWeakDerivAlong.mul_of_locally_bounded.

Source excerpt, lines 567–577 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Calculus

universe u
open MeasureTheory Set Filter Metric

Formal statement


theorem FunctionalInequalities.Analysis.hasWeakDerivAlong_exp_neg_of_lipschitz_readable {E : Type u}
    [instNormedAddCommGroup : NormedAddCommGroup E]
    [instInnerProductSpace : InnerProductSpace ℝ E]
    [instFiniteDimensional : FiniteDimensional ℝ E]
    [instMeasurableSpace : MeasurableSpace E] [instBorelSpace : BorelSpace E]
    {F : E → ℝ} {L : NNReal} (hF : LipschitzWith L F) (v : E) :
    HasWeakDerivAlong (fun x => Real.exp (-F x))
      (fun x => -Real.exp (-F x) * fderiv ℝ F x v) v ∧
    ∀ S : Set E, IsCompact S →
      MemLp (fun x => -Real.exp (-F x) * fderiv ℝ F x v) 2
        ((volume : Measure E).restrict S) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/WeakDerivative/Calculus.lean#L564-L659 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.WeakDerivative.Calculus`, declaration `FunctionalInequalities.Analysis.hasWeakDerivAlong_exp_neg_of_lipschitz`; the repository is private at upload time).

View graph