Integrated Hessian Increment Energy Bound

This formalizes part of Theorem 2.5 of Letwin (arXiv:2607.24164v1), in the weak route.

Let $u,V,\eta:\mathbb R^n\to\mathbb R$. Assume: (1) $u,V\in C^1$ and are convex; (2) $\nabla u$ is Lipschitz; (3) $-u+V\circ\nabla u$ is Lipschitz; (4) for some $K>0$, almost everywhere $\nabla^2u(x)$ is positive definite, $\log\det\nabla^2u(x)=-u(x)+V(\nabla u(x))$, and $K I-\nabla^2u(x)$ is positive semidefinite; (5) $\eta\in C_c^2$ and $\eta\ge0$; and (6) for some $D\in\mathbb R$ and every $x,h$, $u(x+h)+u(x-h)-2u(x)\le D\|h\|^2$.

For every $h\in\mathbb R^n$,

where $H=\operatorname{hessianMatrix}(u)$ and $L\eta=\operatorname{tr}(H^{-1}\operatorname{hessianMatrix}(\eta))-DV(\nabla u)[\nabla\eta]$.

The result is a weak integrated Hessian-increment estimate supporting, but not proving, the cited paper theorem.

Original Lean declaration header

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

theorem integral_mul_hessian_increment_le {n : ℕ} {u V η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) (hconv : ConvexOn ℝ univ u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V) (hVc : ConvexOn ℝ univ V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x))) {K : ℝ} (hK : 0 < K)
    (hdata : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).PosDef ∧
      Real.log (hessianMatrix u x).det = -u x + V (gradient u x) ∧
      (K • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef)
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) (hη0 : ∀ x, 0 ≤ η x) {D : ℝ}
    (h : EuclideanSpace ℝ (Fin n)) (hw : ∀ x, u (x + h) + u (x - h) - 2 * u x ≤ D * ‖h‖ ^ 2) :
    ∫ x, η x * ((∑ i, ∑ j, (hessianMatrix u (x + h) - hessianMatrix u x) i j ^ 2) +
        ∑ i, ∑ j, (hessianMatrix u (x - h) - hessianMatrix u x) i j ^ 2) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) ≤
      2 * K ^ 2 * (D * ‖h‖ ^ 2) *
        ∫ x, |η x + (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
          fderiv ℝ V (gradient u x) (gradient η x))| * Real.exp (-u x)
          ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/Convex/HessianIncrement.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates.

Selected supporting theorems: ae_hessian_increment_le_generator, centeredDifference_contDiff_lipschitz_gradient, centeredDifference_nonneg_le, integrable_hessian_increment_energy, integrable_weak_generator_densities.

Previous: integrable_hessian_increment_energy · Next: exists_hessian_cutoff_sq_difference_bound.

Source excerpt, lines 116–132 · Frozen source 408915f.