OAI/Geometry/RCD/Transport/RadialMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A radial transport plan with a controlled midpoint

The second marginal is constructed by normalized balls shrinking to the pole. The asymmetric CD estimate controls the midpoint independently of those ball densities; compactness then gives the actual Dirac endpoint.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_radial_midpoint_plan line 20