OAI/Geometry/RCD/Transport/OptimalCommonContactSet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One contact set for all optimal plans with fixed endpoints

The same optimal dual pair contacts every optimal coupling. Consequently the compact set used for length localization can be fixed before replacing or refining any segment of a plan.

  1. theorem OAI.RegularPointCoordinates.optimalPlan_contact_transfer line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.common_optimal_length_set line 51