OAI/Geometry/RCD/Transport/OptimalDualSaturation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every cost-minimizing coupling saturates the same dual pair

  1. theorem OAI.RegularPointCoordinates.compact_dual_saturation_of_cost_le line 15