OAI/Geometry/RCD/Transport/TripletTransportCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quadratic transport costs of the two legs of a geodesic triplet law

  1. theorem OAI.RegularPointCoordinates.transportCost_map_scale line 14