OAI/Geometry/RCD/Transport/RenyiOptimalMidpoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rényi-maximizing optimal midpoints

Compactness of actual optimal geodesic plans and the full-measure dual formula give maximizers without assuming a density for the maximizer.

  1. theorem OAI.RegularPointCoordinates.exists_optimal_geodesic_plan_maximizing_renyi line 18
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_renyi_maximizing_midpoint line 37