Gradient of a Linear Perturbation

Proved

FunctionalInequalities.Analysis.BakryEmery.gradient_sub_inner_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This pointwise differential identity computes the gradient after subtracting a linear functional.

Let $E$ be a complete real inner-product space, let $V:E\to\mathbb R$ , and let $z,x\in E$ . If $V$ is differentiable at $x$ , then

\nabla\bigl(V-\langle z,\cdot\rangle\bigr)(x)=\nabla V(x)-z.

The statement uses gradient and requires only differentiability of $V$ at the specified point. It is the basic calculus identity used when differentiating tilted potentials.

Original Lean declaration header

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

theorem gradient_sub_inner {V : E → ℝ} (z x : E) (hV : DifferentiableAt ℝ V x) :
    gradient (fun y => V y - ⟪z, y⟫) x = gradient V x - z

Module navigation

Module: Analysis/BakryEmery/Tilt/Basic.

Next: expTilt_tilted.

Source excerpt, lines 61–62 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Basic

open scoped RealInnerProductSpace ContDiff
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.gradient_sub_inner_readable {V : E → ℝ} (z x : E) (hV : DifferentiableAt ℝ V x) :
    gradient (fun y => V y - ⟪z, y⟫) x = gradient V x - z := by sorry

Source

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

View graph