OAI/Geometry/RCD/Transport/CompactDualCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A saturated dual pair minimizes the compact transport cost

  1. theorem OAI.RegularPointCoordinates.coupling_potential_integral line 16
  2. theorem OAI.RegularPointCoordinates.compact_dual_cost_minimizer line 38