Prove2Me

Gradient Pairing with the Laplacian

Proved
FunctionalInequalities.Analysis.BakryEmery.inner_gradient_gradient_laplacian_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a pointwise third-order derivative identity.

Let EE be a complete finite-dimensional real inner-product space, let f:E→Rf:E\to\mathbb R be C3C^3, and let x∈Ex\in E. With eie_i denoting the fixed standard orthonormal basis,

⟨∇f(x),∇(Δf)(x)⟩=∑j∂jf(x)∑i∂i∂i∂jf(x).\langle\nabla f(x),\nabla(\Delta f)(x)\rangle = \sum_j \partial_jf(x)\sum_i \partial_i\partial_i\partial_j f(x).

In the formal expression, the inner sum is written by applying the derivative to y↦∂i∂jf(y)y\mapsto \partial_i\partial_j f(y) in the direction eie_i; equality uses commutation of third derivatives. This is an auxiliary identity for local Bochner formulas.

Original Lean declaration header

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

theorem inner_gradient_gradient_laplacian {f : E → ℝ} (hf : ContDiff ℝ 3 f) (x : E) :
    ⟪gradient f x, gradient (Laplacian.laplacian f) x⟫ =
      ∑ j, fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
        ∑ i, fderiv ℝ (fun y => fderiv ℝ (fun z => fderiv ℝ f z (stdOrthonormalBasis ℝ E j)) y
          (stdOrthonormalBasis ℝ E i)) x (stdOrthonormalBasis ℝ E i)

Module navigation

Module: Analysis/BakryEmery/Bochner/Basic.

Previous: laplacian_norm_gradient_sq · Next: inner_gradient_gradient_inner.

Source excerpt, lines 245–249 · 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_laplacian_readable {f : E → ℝ} (hf : ContDiff ℝ 3 f) (x : E) :
    ⟪gradient f x, gradient (Laplacian.laplacian f) x⟫ =
      ∑ j, fderiv ℝ f x (stdOrthonormalBasis ℝ E j) *
        ∑ i, fderiv ℝ (fun y => fderiv ℝ (fun z => fderiv ℝ f z (stdOrthonormalBasis ℝ E j)) y
          (stdOrthonormalBasis ℝ E i)) x (stdOrthonormalBasis ℝ E i) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Bochner/Basic.lean#L244-L260 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Bochner.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.inner_gradient_gradient_laplacian`; the repository is private at upload time).

View graph