OAI/Analysis/RCDHeat/EntropyWassersteinGeodesic.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EntropyWassersteinGeodesic, EntropyDirectional, GeodesicWeakGradient, GeodesicIntegral, CompressionPullback, TestPlanMeasure.

  1. theorem OAI.RegularPointCoordinates.transportCost_plan_eq_integral line 17
  2. theorem OAI.RegularPointCoordinates.FullCD.exists_entropy_wasserstein_geodesic line 31
  3. theorem OAI.RegularPointCoordinates.entropy_plan_signed_secant line 86
  4. theorem OAI.RegularPointCoordinates.FullCD.exists_entropy_directional_plan line 132
  5. theorem OAI.RegularPointCoordinates.norm_deriv_comp_le_localSlope line 178
  6. def OAI.RegularPointCoordinates.geodesicExtension line 222
  7. theorem OAI.RegularPointCoordinates.geodesicExtension_eq line 225
  8. theorem OAI.RegularPointCoordinates.IsGeodesic.extension_lipschitz line 229
  9. theorem OAI.RegularPointCoordinates.localSlope_comp_intervalIntegrable line 258
  10. theorem OAI.RegularPointCoordinates.lipschitz_increment_le_integral_localSlope line 269
  11. theorem OAI.RegularPointCoordinates.IsGeodesic.increment_le_integral_localSlope line 287
  12. def OAI.RegularPointCoordinates.compressionPullback line 308
  13. theorem OAI.RegularPointCoordinates.compressionPullback_ae line 314
  14. theorem OAI.RegularPointCoordinates.compressionPullback_tendsto line 324
  15. theorem OAI.RegularPointCoordinates.compressionPullback_memLp line 332
  16. def OAI.RegularPointCoordinates.testPlanMeasure line 346
  17. def OAI.RegularPointCoordinates.testPlanEval line 348
  18. theorem OAI.RegularPointCoordinates.testPlanEval_continuous line 351
  19. theorem OAI.RegularPointCoordinates.testPlanEval_measurable line 355
  20. theorem OAI.RegularPointCoordinates.testPlanMeasure_compression line 360
  21. theorem OAI.RegularPointCoordinates.testPlanMeasure_eval_memLp line 377