OAI/Geometry/RCD/Transport/PointedTransportMarginals.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Affine Euclidean limits of the actual source transport marginals

Once the endpoint-pair laws converge, every fixed intermediate-time law converges to the affine interpolation of that same limiting pair law.

  1. theorem OAI.RegularPointCoordinates.pointed_transport_marginals_tendsto line 20