Lipschitz Monge–Ampère Exponent

Proved

FunctionalInequalities.Analysis.exists_lipschitzWith_neg_add_comp_gradient_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is a regularity lemma for the Monge–Ampère exponent.

Let $u,V:\mathbb R^n\to\mathbb R$ . Assume that $u$ is globally Lipschitz with constant $L$ , $\nabla u$ is globally Lipschitz with constant $G$ , and $V\in C^1$ . Then there exists $L_F\in[0,\infty)$ such that

x\longmapsto -u(x)+V(\nabla u(x))

is globally $L_F$ -Lipschitz. The result is dimension-finite but applies to every $n\in\mathbb N$ and supplies the exponent regularity used by later weak Monge–Ampère identities.

Original Lean declaration header

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

theorem exists_lipschitzWith_neg_add_comp_gradient {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {L G : NNReal}
    (hL : LipschitzWith L u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V) :
    ∃ LF : NNReal, LipschitzWith LF (fun x => -u x + V (gradient u x))

Module navigation

Module: Analysis/Lipschitz/Gradient.

Source excerpt, lines 12–16 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Lipschitz_Gradient

Formal statement


theorem FunctionalInequalities.Analysis.exists_lipschitzWith_neg_add_comp_gradient_readable {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {L G : NNReal}
    (hL : LipschitzWith L u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V) :
    ∃ LF : NNReal, LipschitzWith LF (fun x => -u x + V (gradient u x)) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Lipschitz/Gradient.lean#L11-L31 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Lipschitz.Gradient`, declaration `FunctionalInequalities.Analysis.exists_lipschitzWith_neg_add_comp_gradient`; the repository is private at upload time).

View graph