Almost-Everywhere Hessian Increment Coercivity

This is a partial formalization of the Hessian coercivity statement associated with Lemma 2.4 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb N$ and let $u,V:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$. Assume:

1. $u$ is $C^1$ and $\nabla u$ is Lipschitz.
2. $V$ is differentiable and convex on the whole space.
3. For almost every $x$, with $H(x)=\operatorname{hessianMatrix}(u,x)$, $H(x)$ is positive definite,

$$\log\det H(x)=-u(x)+V(\nabla u(x)),$$

and $K I-H(x)$ is positive semidefinite.

For every increment $h$, for almost every $x$,

$$\frac{\|H(x+h)-H(x)\|_F^2+\|H(x-h)-H(x)\|_F^2}{2K^2} \le \operatorname{tr}\!\left(H(x)^{-1}H_w(x)\right) -DV(\nabla u(x))(\nabla w(x))+w(x),$$

where $w(y)=u(y+h)+u(y-h)-2u(y)$ and $H_w=\operatorname{hessianMatrix}(w,\cdot)$. The almost-everywhere qualifier is with respect to Lebesgue measure, and no positivity of $K$ is separately assumed.

Original Lean declaration header

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

theorem ae_hessian_increment_le_generator {n : ℕ} {u V : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hV : Differentiable ℝ V) (hVc : ConvexOn ℝ univ V) {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 : EuclideanSpace ℝ (Fin n)) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ((∑ i, ∑ j, (hessianMatrix u (x + h) - hessianMatrix u x) i j ^ 2) +
          ∑ i, ∑ j, (hessianMatrix u (x - h) - hessianMatrix u x) i j ^ 2) / (2 * K ^ 2) ≤
        ((hessianMatrix u x)⁻¹ *
            hessianMatrix (fun y => u (y + h) + u (y - h) - 2 * u y) x).trace -
          fderiv ℝ V (gradient u x) (gradient (fun y => u (y + h) + u (y - h) - 2 * u y) x) +
          (u (x + h) + u (x - h) - 2 * u x)

Module navigation

Module: Analysis/Convex/Viscosity.

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

Supporting theorems: log_det_add_frobenius_sq_le.

Previous: exists_penalized_maximum_with_comparison.

Source excerpt, lines 1920–1934 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Viscosity

open FunctionalInequalities.Probability.Stein
open MeasureTheory Set Filter

theorem FunctionalInequalities.Analysis.ae_hessian_increment_le_generator_readable {n : ℕ} {u V : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hV : Differentiable ℝ V) (hVc : ConvexOn ℝ univ V) {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 : EuclideanSpace ℝ (Fin n)) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ((∑ i, ∑ j, (hessianMatrix u (x + h) - hessianMatrix u x) i j ^ 2) +
          ∑ i, ∑ j, (hessianMatrix u (x - h) - hessianMatrix u x) i j ^ 2) / (2 * K ^ 2) ≤
        ((hessianMatrix u x)⁻¹ *
            hessianMatrix (fun y => u (y + h) + u (y - h) - 2 * u y) x).trace -
          fderiv ℝ V (gradient u x) (gradient (fun y => u (y + h) + u (y - h) - 2 * u y) x) +
          (u (x + h) + u (x - h) - 2 * u x) := by sorry