Partial differential equations · Result 374

Sharp one-third stability of Brenier maps

1 paperLean

For uniform source measure ρ on a compact convex body with interior in dimension at least two, quadratic optimal transport maps satisfy \(\|T_\mu-T_\nu\|_{L^2(\rho)}\le C W_2(\mu,\nu)^{1/3}\) uniformly over targets in a fixed compact set. The exponent is sharp, even for three-atom targets, disproving Letrouit's conjectured square-root bound.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 1

Sharp One-Third Stability of Brenier Maps

OpenAI · September 25, 2026

For the uniform probability measure ρ on a compact convex body in ℝ^d, d ≥ 2, quadratic optimal transport maps are one-third Hölder continuous in \(L^2(\rho)\) with respect to the target's 2-Wasserstein distance. The constant is uniform over all targets supported in a fixed compact set, and the exponent is optimal. A three-atom family on a fixed cube disproves Letrouit's conjectured uniform square-root estimate.

Read PDF Download Source

Cite

@misc{OAI:Sharp-One-Third-Stability-of-Brenier-Maps-September-25-2026,
  author = {{OpenAI}},
  title = {{Sharp One-Third Stability of Brenier Maps}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-One-Third-Stability-of-Brenier-Maps-September-25-2026/article.pdf}{OAI:Sharp-One-Third-Stability-of-Brenier-Maps-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):

Sharp One-Third Stability of Brenier Maps

Scope

The formalization proves one-third Hölder stability of Brenier maps from the uniform measure on a compact convex body with nonempty interior in \(\mathbb R^d\), for every \(d\ge2\). For targets supported in one fixed nonempty compact set, the \(L^2\) distance between the unique quadratic optimal maps is at most a constant times the one-third power of the targets' \(2\)-Wasserstein distance. The constant is uniform over those targets.

It also proves optimality of the exponent: on a fixed cube, pairs of three-atom target measures violate every analogous bound with exponent greater than \(1/3\). In particular, the conjectured uniform square-root estimate fails.

Comparator links

Result	Comparator statement
One-third stability of Brenier maps and sharpness	Brenier.lean

Scope note on GitHub →