Weak Derivative of the First Monge–Ampère Right-Hand Side

Proved

FunctionalInequalities.Analysis.hasWeakDerivAlong_mongeAmpere_first_rhs_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is the weak derivative formula for the first Monge–Ampère right-hand side, corresponding to part of Lemma 2.4 of Letwin (arXiv:2607.24164v1).

Let $u$ be $C^1$ with Lipschitz $u$ and Lipschitz gradient, let $W$ be $C^2$ , and let $T$ be a tensor of compact-local $L^2$ weak derivatives of the Hessian $H_u$ . For every $i,j$ , the function

-\partial_i u+\sum_a H_{ia}\,\partial_aW(\nabla u)

has weak derivative along $e_j$ equal to

-H_{ji}+\sum_a\left(T_{jia}\,\partial_aW(\nabla u) +H_{ia}\sum_b H_{jb}\,\partial_{ba}W(\nabla u)\right).

The derivative density belongs locally to $L^2$ on every compact set. No $C^2$ regularity of $u$ is assumed.

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.

            hessianMatrix u x i a *
              ∑ b : Fin n, hessianMatrix u x j b * hessianMatrix W (gradient u x) b a))
        (EuclideanSpace.basisFun (Fin n) ℝ j) ∧
      ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp
          (fun x => -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))
          2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.

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

Selected supporting theorems: HasWeakDerivAlong.congr_ae, HasWeakDerivAlong.mul_of_locally_bounded, exists_lipschitzWith_weak_fderiv_comp_gradient, hasWeakDerivAlong_finsetSum_mul, hasWeakDerivAlong_of_lipschitz.

Previous: exists_lipschitzWith_weak_fderiv_comp_gradient · Next: localLp_hessian_flux_trace_forcing.

Source excerpt, lines 407–418 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_WeakHessianEvolution

open MeasureTheory Set Filter
open FunctionalInequalities.Probability.Stein
set_option maxHeartbeats 800000

Formal statement


theorem FunctionalInequalities.Analysis.hasWeakDerivAlong_mongeAmpere_first_rhs_readable {n : ℕ}
    {u W : EuclideanSpace ℝ (Fin n) → ℝ}
    {L G : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u)
    (hG : LipschitzWith G (gradient u)) (hW : ContDiff ℝ 2 W)
    (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)) :
    ∀ i j : Fin n,
      HasWeakDerivAlong
        (fun x => -fderiv ℝ u x (EuclideanSpace.basisFun (Fin n) ℝ i) +
          ∑ a : Fin n, hessianMatrix u x i a *
            fderiv ℝ W (gradient u x) (EuclideanSpace.basisFun (Fin n) ℝ a))
        (fun x => -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))
        (EuclideanSpace.basisFun (Fin n) ℝ j) ∧
      ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
        MemLp
          (fun x => -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))
          2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma 2.4. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.lean#L382-L460 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.IntegrationByParts.WeakHessianEvolution`, declaration `FunctionalInequalities.Analysis.hasWeakDerivAlong_mongeAmpere_first_rhs`; the repository is private at upload time).

View graph