Mean Hessian Identity for a Lipschitz Gradient

This formalizes the analytic part of Lemma 2.3 of Letwin (arXiv:2607.24164v1).

Let $E$ be a finite-dimensional real inner-product space and let $\phi:E\to\mathbb R$. Assume:

1. $\phi$ is $C^1$.
2. For some $G\in[0,\infty)$, the gradient $\nabla\phi$ is $G$-Lipschitz.
3. $\phi$ is convex on $E$.
4. $e^{-\phi}$ is integrable with respect to volume measure and

$$\int_E e^{-\phi(x)}\,dx=1.$$

5. The gradient belongs to $L^2(\nu)$, where $\nu=\operatorname{volume}.\operatorname{tilted}(-\phi)$.

Then, for all $u,v\in E$,

$$\int_E\left\langle D(\nabla\phi)(x)[u],v\right\rangle\,d\nu(x)=\int_E D\phi(x)[u]D\phi(x)[v] \,d\nu(x).$$

This identity relates the mean derivative of the Lipschitz gradient to products of directional derivatives and is useful in tilted integration-by-parts calculations.

Formalization Note. The derivative of $\nabla\phi$ is the pointwise Fréchet derivative supplied by fderiv; the equality is integrated against the normalized tilted measure.

Original Lean declaration header

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

theorem integral_inner_fderiv_gradient_tilted_eq_integral_fderiv_mul (φ : E → ℝ)
    (hφ : ContDiff ℝ 1 φ) {G : NNReal} (hG : LipschitzWith G (gradient φ))
    (hc : ConvexOn ℝ Set.univ φ)
    (hexp : Integrable (fun x => Real.exp (-φ x)) (volume : Measure E))
    (hnorm : ∫ x, Real.exp (-φ x) ∂(volume : Measure E) = 1)
    (hgrad : MemLp (gradient φ) 2 ((volume : Measure E).tilted (-φ))) (u v : E) :
    (∫ x, ⟪fderiv ℝ (gradient φ) x u, v⟫ ∂((volume : Measure E).tilted (-φ))) =
      ∫ x, fderiv ℝ φ x u * fderiv ℝ φ x v ∂((volume : Measure E).tilted (-φ))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/LipschitzHessian.

Supporting theorems: hasWeakDerivAlong_of_lipschitz.

Next: integral_fderiv_tilted_eq_integral_mul_fderiv_of_bounded_lipschitz.

Source excerpt, lines 30–37 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_LipschitzHessian

open MeasureTheory Filter Topology
open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
set_option maxHeartbeats 800000

theorem FunctionalInequalities.Analysis.BakryEmery.integral_inner_fderiv_gradient_tilted_eq_integral_fderiv_mul_readable (φ : E → ℝ)
    (hφ : ContDiff ℝ 1 φ) {G : NNReal} (hG : LipschitzWith G (gradient φ))
    (hc : ConvexOn ℝ Set.univ φ)
    (hexp : Integrable (fun x => Real.exp (-φ x)) (volume : Measure E))
    (hnorm : ∫ x, Real.exp (-φ x) ∂(volume : Measure E) = 1)
    (hgrad : MemLp (gradient φ) 2 ((volume : Measure E).tilted (-φ))) (u v : E) :
    (∫ x, ⟪fderiv ℝ (gradient φ) x u, v⟫ ∂((volume : Measure E).tilted (-φ))) =
      ∫ x, fderiv ℝ φ x u * fderiv ℝ φ x v ∂((volume : Measure E).tilted (-φ)) := by sorry