OAI/Geometry/RCD/Transport/OptimalLengthLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Length labels survive optimal-plan replacement

An interior marginal fixes the joint law of position and total geodesic length. Consequently every measurable length restriction has the same interior marginal before and after replacement.

  1. theorem OAI.RegularPointCoordinates.eval_length_law line 19
  2. theorem OAI.RegularPointCoordinates.length_restriction_eval line 30
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_eval_length_law_eq line 41
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_length_restriction_eval_eq line 59