Coordinate Chain Rule Through the Gradient Map

Proved

FunctionalInequalities.Probability.Stein.chain_coordinate_of_differentiableAt_gradient_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This statement gives a coordinate chain rule for a composition with a gradient map.

Let $n\in\mathbb N$ and let $u,f:\mathbb R^n\to\mathbb R$ be $C^1$ . At a point $y\in\mathbb R^n$ , assume that $∇u$ is differentiable at $y$ . For every coordinate $i\in\operatorname{Fin}(n)$ ,

D_{e_i}(f\circ∇u)(y) = \sum_j (\nabla^2u(y))_{ij}\,(\nabla f(\nabla u(y)))_j.

Here hessianMatrix u y is the matrix used for the weak Hessian coordinates. The result is a finite-dimensional pointwise identity and makes no global invertibility claim about $∇u$ .

Original Lean declaration header

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

theorem chain_coordinate_of_differentiableAt_gradient {n : ℕ}
    {u f : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u)
    (hf : ContDiff ℝ 1 f) {y : EuclideanSpace ℝ (Fin n)}
    (hy : DifferentiableAt ℝ (gradient u) y) (i : Fin n) :
    fderiv ℝ (f ∘ gradient u) y (EuclideanSpace.basisFun (Fin n) ℝ i) =
      ∑ j, hessianMatrix u y i j * gradient f (gradient u y) j

Module navigation

Module: Analysis/BakryEmery/WeakHessian.

Definition modules: Analysis/BakryEmery/HessianOperator.

Previous: memLp_cutoff_mul_hessianMatrix_entry.

Source excerpt, lines 504–509 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_WeakHessian

set_option maxHeartbeats 400000

Formal statement


theorem FunctionalInequalities.Probability.Stein.chain_coordinate_of_differentiableAt_gradient_readable {n : ℕ}
    {u f : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u)
    (hf : ContDiff ℝ 1 f) {y : EuclideanSpace ℝ (Fin n)}
    (hy : DifferentiableAt ℝ (gradient u) y) (i : Fin n) :
    fderiv ℝ (f ∘ gradient u) y (EuclideanSpace.basisFun (Fin n) ℝ i) =
      ∑ j, hessianMatrix u y i j * gradient f (gradient u y) j := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma 2.7 (Fathi [29, Theorem 2.3]). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/WeakHessian.lean#L501-L535 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.WeakHessian`, declaration `FunctionalInequalities.Probability.Stein.chain_coordinate_of_differentiableAt_gradient`; the repository is private at upload time).

View graph