OAI/Geometry/RCD/Transport/OptimalInitialSubmeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint preservation of length classes for optimal submeasures

Compression of the reference plan gives its initial Kantorovich speed. Thus the initial component marginal already fixes every measurable length class, without prescribing an interior marginal of the competitor.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_initial_submeasure_length_transfer line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_distance_bound line 45