we-solve (beta)

Math-2837-A1 · revision r1 · on Math-2837

OpenAI claim summary for Math-2837

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Sharp one-third Brenier stability: The source is the uniform measure of one fixed convex body, and all targets share one compact support bound. Atomic targets are allowed; the three-atom construction rules out every exponent above $1/3$ in this uniform setting.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. The optimal one-third stability exponent for compact-target Brenier maps
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

The optimal one-third stability exponent for compact-target Brenier maps

OpenAI's claim

Sharp one-third Brenier stability: The paper claims a uniform $L^2$ stability estimate with exponent $1/3$ for quadratic optimal maps from a uniform convex-body source to targets in a fixed compact set. A three-atom family shows that larger exponents, including the proposed square-root estimate, fail.

Mathematical statement of the claimed result

Mathematical claim 1.
Fix $d\ge2$, a compact convex $K\subset\mathbb R^d$ with nonempty interior, uniform source probability $\rho=\mathbf1_Kdx/|K|$, and nonempty compact target set $Y$. For the quadratic-cost Brenier maps $T_\mu$ to arbitrary probability measures $\mu$ on $Y$, the claimed uniform stability is \[\|T_\mu-T_\nu\|_{L^2(\rho)}\le C(K,Y)W_2(\mu,\nu)^{1/3}.\] Here $W_2$ minimizes the root-mean-square distance over couplings. Atomic, singular and absolutely continuous targets are all permitted. The exponent is asserted optimal: no larger exponent works uniformly, even with $K=Y=[-1,1]^d$ and three-atom targets.

Outline of the argument

Sharp one-third Brenier stability: In the obstruction, tilting one plane in a three-plane maximum switches a thin source cell between separated target slopes while preserving its mass. For the upper estimate, semi-discrete cell calculus tracks cell masses and first moments as slopes and intercepts vary. The central moment comparison controls the map difference, and approximation extends the estimate to arbitrary compactly supported targets.

Formal verification

Family 374 describes Lean coverage for uniform one-third map stability and its optimality through three-atom targets.

Sharp one-third Brenier stability: The manuscript links Brenier.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources