Weak MTW curvature gives convexity and regular optimal transport

2 papersLean

On every closed connected Riemannian manifold of dimension at least two satisfying weak Ma–Trudinger–Wang curvature, all tangent injectivity domains are convex, resolving Villani’s conjecture in this setting. For squared-distance transport between measurable probability densities bounded above and away from zero, the optimal map and its inverse are Hölder continuous.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Global Support and Convex Injectivity Domains under Weak MTW

OpenAI · September 25, 2026

We prove that weak Ma–Trudinger–Wang curvature on a smooth, connected, compact Riemannian manifold of dimension at least two without boundary implies convexity of every tangent injectivity domain, resolving Villani's conjecture in this setting. Conjugate cut points are allowed. More generally, every ordinary subgradient of a squared-distance cost potential is a minimizing velocity with a global supporting mountain. No density hypothesis is used.

Read PDF Download Source

Cite

@misc{OAI:Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026,
  author = {{OpenAI}},
  title = {{Global Support and Convex Injectivity Domains under Weak MTW}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf}{OAI:Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026}},
  year = {2026}
}

Uniform Bi-Holder Transport from Weak MTW

OpenAI · September 25, 2026

We prove that the weak Ma–Trudinger–Wang condition on a fixed smooth connected compact boundaryless Riemannian manifold of dimension at least two implies a common Hölder estimate for optimal transport maps and their inverses over the entire class of probability densities with fixed positive upper and lower bounds. The maps have homeomorphic representatives, conjugate cut points are allowed, and no density regularity is assumed.

Read PDF Download Source

Cite

@misc{OAI:Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026,
  author = {{OpenAI}},
  title = {{Uniform Bi-H{\"o}lder Transport from Weak MTW}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026/paper.pdf}{OAI:Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

On a compact connected smooth Riemannian manifold of dimension at least two, the formalized result proves that weak MTW curvature implies convexity of every open tangent injectivity domain. Prior convexity or nonfocality is not assumed. Additional formalized results give global support at ordinary subgradients, compact convex lifted gap sections with the stated diameter bound, and scale and local-injectivity estimates for finite target families. The latter finite-family result does not cover the paper's arbitrary-potential local-injectivity assertion.

The formalized result gives uniform bi-Hölder optimal transport for squared-distance cost on each fixed compact connected smooth Riemannian manifold of dimension at least two satisfying weak MTW. For probability densities between fixed positive lower and finite upper bounds, one exponent and constant work for every pair of densities. The optimal map is a homeomorphism, is unique almost everywhere, and both it and its inverse satisfy the global Hölder bound. The constants are uniform over the density class on the fixed manifold, not over varying metrics.

Comparator links

Result	Comparator statement
Convex injectivity domains under weak MTW	WeakMTWGlobalSupport.lean
Uniform bi-Hölder optimal transport	BiholderTransport.lean

Scope note on GitHub →