Prove2Me

Gradient Pairing Product-Rule Identity

Proved
FunctionalInequalities.Analysis.BakryEmery.inner_gradient_gradient_inner_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a pointwise second-derivative identity for the drift term in the local Bochner calculation.

Let EE be a complete finite-dimensional real inner-product space, let U,f:E→RU,f:E\to\mathbb R be respectively C2C^2, and let x∈Ex\in E. Write eie_i for the fixed standard orthonormal basis of EE. Then

⟨∇f(x),∇⟨∇U,∇f⟩(x)⟩=D2U(x)(∇f(x),∇f(x))+∑i∑j∂iU(x) ∂jf(x) D2f(x)(ei,ej).\left\langle \nabla f(x),\nabla\langle\nabla U,\nabla f\rangle(x)\right\rangle = D^2U(x)(\nabla f(x),\nabla f(x)) +\sum_i\sum_j \partial_iU(x)\,\partial_jf(x)\,D^2f(x)(e_i,e_j).

The Hessian is represented by bilinearIteratedFDerivTwo, and the sums use stdOrthonormalBasis ℝ E. This technical identity is reusable in pointwise Bochner expansions.

Original Lean declaration header

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

theorem inner_gradient_gradient_inner {U f : E → ℝ} (hU : ContDiff ℝ 2 U) (hf : ContDiff ℝ 2 f)
    (x : E) :
    ⟪gradient f x, gradient (fun y => ⟪gradient U y, gradient f y⟫) x⟫ =
      bilinearIteratedFDerivTwo ℝ U x (gradient f x) (gradient f x) +
        ∑ i, ∑ j, fderiv ℝ U x (stdOrthonormalBasis ℝ E i) *
          fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
          bilinearIteratedFDerivTwo ℝ f x (stdOrthonormalBasis ℝ E i)
            (stdOrthonormalBasis ℝ E j)

Module navigation

Module: Analysis/BakryEmery/Bochner/Basic.

Previous: inner_gradient_gradient_laplacian · Next: gammaTwo_eq_hessianSqStdBasis_add.

Source excerpt, lines 264–271 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Bochner_Basic

open scoped ContDiff RealInnerProductSpace
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [CompleteSpace E] [FiniteDimensional ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.inner_gradient_gradient_inner_readable {U f : E → ℝ} (hU : ContDiff ℝ 2 U) (hf : ContDiff ℝ 2 f)
    (x : E) :
    ⟪gradient f x, gradient (fun y => ⟪gradient U y, gradient f y⟫) x⟫ =
      bilinearIteratedFDerivTwo ℝ U x (gradient f x) (gradient f x) +
        ∑ i, ∑ j, fderiv ℝ U x (stdOrthonormalBasis ℝ E i) *
          fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
          bilinearIteratedFDerivTwo ℝ f x (stdOrthonormalBasis ℝ E i)
            (stdOrthonormalBasis ℝ E j) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Bochner/Basic.lean#L262-L286 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Bochner.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.inner_gradient_gradient_inner`; the repository is private at upload time).

View graph