Almost-Everywhere Hessian Flux Forcing Decomposition

Proved

FunctionalInequalities.Analysis.ae_hessian_flux_forcing_minus_drift_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an almost-everywhere algebraic identity associated with the weak second Hessian evolution.

Let $u,W:\mathbb R^n\to\mathbb R$ be such that $u$ is $C^1$ with Lipschitz gradient, $W$ is $C^2$ , and $-u+W\circ\nabla u$ is Lipschitz. Assume

\det\nabla^2u(x)=\exp\bigl(-u(x)+W(\nabla u(x))\bigr)

a.e. Assume a weak Hessian tensor $T$ and weak inverse-Hessian derivatives with the compact-local $L^2$ and ENNReal-valued local $L^\infty$ hypotheses stated in the declaration.

With

R=(\nabla^2u)^{-1},\quad D_{kba}=-(RT_kR)_{ba},\quad J_{ija}=\sum_bR_{ba}T_{bij},

and

Q_{ij}=-(\nabla^2u)_{ji}+\sum_a\left(T_{jia}\,\partial_aW(\nabla u) +(\nabla^2u)_{ia}\sum_b(\nabla^2u)_{jb}(\nabla^2W)_{ba}(\nabla u)\right),

the following equality holds for almost every $x$ , simultaneously for all $i,j$ :

Q_{ij}-\sum_{a,b}T_{iab}D_{jba} +\sum_bT_{bij}\sum_aD_{aba} -\sum_aJ_{ija}\,\partial_a u = -(\nabla^2u)_{ij} +(\nabla^2u\,\nabla^2W(\nabla u)\,\nabla^2u)_{ij} +\operatorname{tr}(RT_iRT_j).

This lemma identifies the forcing term needed to convert the unweighted weak flux identity into the weighted curvature–Gram identity.

Original Lean conclusion excerpt

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Earlier hypotheses and the proof are omitted from this excerpt; the complete verified statement remains below.

    let Q := fun x i j => -hessianMatrix u x j i + ∑ a : Fin n,
      (T x j i a * fderiv ℝ W (gradient u x) (EuclideanSpace.basisFun (Fin n) ℝ a) +
        hessianMatrix u x i a * ∑ b : Fin n, hessianMatrix u x j b *
          hessianMatrix W (gradient u x) b a)
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), ∀ i j : Fin n,
      Q x i j - (∑ a : Fin n, ∑ b : Fin n, T x i a b * D x j b a) +
        (∑ b : Fin n, T x b i j * (∑ a : Fin n, D x a b a)) -
        (∑ a : Fin n, J x i j a * fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ a)) =
      -hessianMatrix u x i j +
        (hessianMatrix u x * hessianMatrix W (gradient u x) * hessianMatrix u x) i j +
        (R x * (Matrix.of fun a b => T x i a b) * R x *
          (Matrix.of fun a b => T x j a b)).trace

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.

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

Supporting theorems: ae_fderiv_mongeAmpere_exponent, ae_inverse_hessian_row_divergence_of_weak_derivative, ae_weak_third_derivative_symm.

Previous: integral_weak_hessian_flux_eq_trace_derivative · Next: integral_exp_neg_flux_of_unweighted.

Source excerpt, lines 1228–1239 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_WeakHessianEvolution

open Matrix MeasureTheory Set Filter
open FunctionalInequalities.Probability.Stein
set_option maxHeartbeats 1200000

Formal statement

 theorem FunctionalInequalities.Analysis.ae_hessian_flux_forcing_minus_drift_readable {n : ℕ}
    {u W : EuclideanSpace ℝ (Fin n) → ℝ} {G LF : NNReal}
    (hu : ContDiff ℝ 1 u)
    (hG : LipschitzWith G (gradient u)) (hW : ContDiff ℝ 2 W)
    (hF : LipschitzWith LF (fun x => -u x + W (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + W (gradient u x)))
    (T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ)
    (hT : ∀ k i j : Fin n,
      HasWeakDerivAlong (fun x => hessianMatrix u x i j) (fun x => T x k i j)
        (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
      ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp (fun x => T x k i j) 2
          ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S))
    (hInv : ∀ k i j : Fin n,
        HasWeakDerivAlong (fun x => (hessianMatrix u x)⁻¹ i j)
          (fun x => -(((hessianMatrix u x)⁻¹ *
            (Matrix.of fun a b => T x k a b) * (hessianMatrix u x)⁻¹) i j))
          (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
        (∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
          MemLp (fun x => -(((hessianMatrix u x)⁻¹ *
            (Matrix.of fun a b => T x k a b) * (hessianMatrix u x)⁻¹) i j))
            2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) ∧
        ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
          MemLp (fun x => (hessianMatrix u x)⁻¹ i j) (⊤ : ENNReal)
            ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    let R := fun x => (hessianMatrix u x)⁻¹
    let D := fun x k b a => -((R x * (Matrix.of fun c d => T x k c d) * R x) b a)
    let J := fun x i j a => ∑ b : Fin n, R x b a * T x b i j
    let Q := fun x i j => -hessianMatrix u x j i + ∑ a : Fin n,
      (T x j i a * fderiv ℝ W (gradient u x) (EuclideanSpace.basisFun (Fin n) ℝ a) +
        hessianMatrix u x i a * ∑ b : Fin n, hessianMatrix u x j b *
          hessianMatrix W (gradient u x) b a)
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), ∀ i j : Fin n,
      Q x i j - (∑ a : Fin n, ∑ b : Fin n, T x i a b * D x j b a) +
        (∑ b : Fin n, T x b i j * (∑ a : Fin n, D x a b a)) -
        (∑ a : Fin n, J x i j a * fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ a)) =
      -hessianMatrix u x i j +
        (hessianMatrix u x * hessianMatrix W (gradient u x) * hessianMatrix u x) i j +
        (R x * (Matrix.of fun a b => T x i a b) * R x *
          (Matrix.of fun a b => T x j a b)).trace := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.lean#L1198-L1280 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.WeakHessianEvolution`, declaration `_private.FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.WeakHessianEvolution.0.FunctionalInequalities.Analysis.ae_hessian_flux_forcing_minus_drift`; the repository is private at upload time).

View graph