OAI/Analysis/RCDHeat/MetricDescentSlope.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: MetricDescentSlope, HeatFullSlope, HeatFullDissipation, HeatEDE, WassersteinGeodesic.

  1. def OAI.RegularPointCoordinates.descentSlope line 18
  2. theorem OAI.RegularPointCoordinates.descentSlope_le_quadratic line 22
  3. theorem OAI.RegularPointCoordinates.le_descentSlope_of_right_speed line 45
  4. def OAI.RegularPointCoordinates.finiteEntropyDomain line 97
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_finite_entropy_slope line 102
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_full_slope_dissipation line 160
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_EDE line 212
  8. theorem OAI.RegularPointCoordinates.geodesic_plan_cost_root line 296
  9. theorem OAI.RegularPointCoordinates.wassersteinEDist_plan_le line 313
  10. theorem OAI.RegularPointCoordinates.wassersteinEDist_geodesic_plan line 332