OAI/Analysis/RCDHeat/CrossingOptimal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CrossingOptimal, ReversePlan, CrossingForward.

  1. lemma OAI.RegularPointCoordinates.transportCost_map_pair line 22
  2. lemma OAI.RegularPointCoordinates.crossing_optimal_lengths line 34
  3. def OAI.RegularPointCoordinates.reverseTime line 115
  4. lemma OAI.RegularPointCoordinates.reverseTime_coe line 117
  5. lemma OAI.RegularPointCoordinates.reverseTime_zero line 118
  6. lemma OAI.RegularPointCoordinates.reverseTime_one line 119
  7. lemma OAI.RegularPointCoordinates.reverseTime_reverseTime line 120
  8. def OAI.RegularPointCoordinates.reversePath line 123
  9. lemma OAI.RegularPointCoordinates.reversePath_apply line 125
  10. lemma OAI.RegularPointCoordinates.reversePath_reversePath line 128
  11. lemma OAI.RegularPointCoordinates.measurable_reversePath line 131
  12. lemma OAI.RegularPointCoordinates.isGeodesic_reversePath line 138
  13. lemma OAI.RegularPointCoordinates.IsOptimalCoupling.swap line 148
  14. lemma OAI.RegularPointCoordinates.reversePlan_eval line 163
  15. lemma OAI.RegularPointCoordinates.reversePlan_optimal line 169
  16. lemma OAI.RegularPointCoordinates.IsOptimalCoupling.mixture line 185
  17. lemma OAI.RegularPointCoordinates.crossing_spliced_plan line 212
  18. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.crossing_paths_agree_future line 282