Prove Brenier (openai/math family 374: Sharp one-third stability of optimal transport maps) in Lean 4 with…
Prove Brenier (openai/math family 374: Sharp one-third stability of optimal transport maps) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 374 of the release, Sharp one-third stability of optimal transport maps (Partial…
The task
Context: this statement belongs to family 374 of the release, *Sharp one-third stability of optimal transport maps* (Partial differential equations). The family as a whole: For uniform source measure $\rho$ on a compact convex body with interior in dimension at least two, quadratic optimal transport maps satisfy…
Part of raising-heart/openai-math.