OAI/Analysis/RCDHeat/HeatMetricSpeed.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatMetricSpeed, CouplingGluing, TransportMinkowski, WassersteinTriangle, WassersteinFinite, WassersteinMetric, HeatMetricAC.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_right_transport_speed line 18
  2. theorem OAI.RegularPointCoordinates.exists_glued_measure line 76
  3. theorem OAI.RegularPointCoordinates.transportCost_sqrt_eq_eLpNorm' line 104
  4. theorem OAI.RegularPointCoordinates.transportCost_sqrt_eq_eLpNorm line 108
  5. theorem OAI.RegularPointCoordinates.transportCost_triangle_marginals line 113
  6. theorem OAI.RegularPointCoordinates.exists_coupling_triangle line 133
  7. def OAI.RegularPointCoordinates.wassersteinEDist line 163
  8. theorem OAI.RegularPointCoordinates.wassersteinSq_eq_iInf_coupling line 165
  9. theorem OAI.RegularPointCoordinates.wassersteinEDist_eq_iInf_coupling line 174
  10. theorem OAI.RegularPointCoordinates.wassersteinEDist_le_cost line 180
  11. theorem OAI.RegularPointCoordinates.transportCost_swap line 185
  12. theorem OAI.RegularPointCoordinates.wassersteinEDist_symm line 188
  13. theorem OAI.RegularPointCoordinates.wassersteinSq_self line 202
  14. theorem OAI.RegularPointCoordinates.wassersteinEDist_self line 212
  15. theorem OAI.RegularPointCoordinates.wassersteinEDist_triangle line 215
  16. theorem OAI.RegularPointCoordinates.FiniteSecondMoment.integrable_dist_sq line 235
  17. theorem OAI.RegularPointCoordinates.finite_second_moment_cost line 247
  18. theorem OAI.RegularPointCoordinates.wassersteinSq_finite line 263
  19. theorem OAI.RegularPointCoordinates.wassersteinEDist_finite line 268
  20. theorem OAI.RegularPointCoordinates.coupling_cost_zero_endpoints line 271
  21. theorem OAI.RegularPointCoordinates.wassersteinEDist_eq_zero_iff_optimal line 280
  22. theorem OAI.RegularPointCoordinates.FullCD.wassersteinEDist_eq_zero_iff line 290
  23. def OAI.RegularPointCoordinates.ACWassersteinProbability line 306
  24. instance OAI.RegularPointCoordinates.ACWassersteinProbability.prob line 310
  25. theorem OAI.RegularPointCoordinates.ACWassersteinProbability.finite line 311
  26. def OAI.RegularPointCoordinates.ACWassersteinProbability.metric line 315
  27. theorem OAI.RegularPointCoordinates.absolutelyContinuous_of_dist_le line 333
  28. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatProbability line 356
  29. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_probability_absolutelyContinuous line 370