OAI/Geometry/RCD/Transport/GeodesicPlanTightness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tight endpoint tails give tight geodesic plans

Properness makes the bounded families of geodesics compact. Both endpoint tails control the mass outside those families, uniformly in the sequence.

  1. theorem OAI.RegularPointCoordinates.geodesic_plans_tight_of_endpoint_tails line 20
  2. theorem OAI.RegularPointCoordinates.geodesic_plans_subsequence_of_endpoint_tails line 58