OAI/Geometry/RCD/Transport/OptimalGeodesicLengths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Length localization of optimal geodesics

Two contacting quadratic-cost geodesics which meet at an interior time have the same total length. A bounded RCD optimal plan therefore has a compact full-measure set on which length is constant on every interior evaluation fiber. This is the localization in Rajala, arXiv:1202.6514, Lemma 2.6.

  1. theorem OAI.RegularPointCoordinates.equal_lengths_of_cross_cost line 20
  2. theorem OAI.RegularPointCoordinates.contacting_geodesics_equal_length line 34
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_length_fibers line 68