OAI/Geometry/RCD/Heat/TwoTimeCostLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The infinitesimal time coefficient in the two-time transport estimate

  1. theorem OAI.RegularPointCoordinates.affine_time_difference_tendsto line 11
  2. theorem OAI.RegularPointCoordinates.two_time_cost_ratio_tendsto line 20