OAI/Geometry/RCD/Transport/OptimalSubmeasureLength.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Length labels transfer to submeasures through one interior marginal

The common contact set determines geodesic length from any interior position. Equality of the component marginals at that time therefore preserves each measurable length class under optimal-plan replacement.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_submeasure_length_transfer line 19