OAI/Geometry/RCD/Transport/OptimalLengthObservable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The length of an optimal geodesic is visible at every interior time

On the common compact contact set, length is constant on evaluation fibers. The quotient map and Tietze extension give one continuous spatial observable for every optimal plan with the prescribed endpoints. This retains variable length weights when segments of the plan are replaced.

  1. theorem OAI.RegularPointCoordinates.compact_length_observable line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.common_optimal_length_observable line 49