OAI/Geometry/RCD/Transport/OptimalRadialMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An optimal replacement to a radial midpoint remains radial

The finite quadratic transport cost and the midpoint marginal determine both radial moments. Equality in the integrated triangle inequality therefore forces the same pole on every replacement path.

  1. theorem OAI.RegularPointCoordinates.optimal_radial_midpoint line 20