OAI/Analysis/RCDHeat/DynamicalPlan.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: DynamicalPlan, BallComparison.

  1. theorem OAI.RegularPointCoordinates.measurable_path_eval line 24
  2. theorem OAI.RegularPointCoordinates.optimalPlan_endpoints line 28
  3. theorem OAI.RegularPointCoordinates.FullCD.support_volume_bound line 39
  4. def OAI.RegularPointCoordinates.midpointFloor line 93
  5. theorem OAI.RegularPointCoordinates.midpointFloor_pos line 96
  6. theorem OAI.RegularPointCoordinates.midpointFloor_ne_top line 100
  7. theorem OAI.RegularPointCoordinates.midpointFloor_le_half line 103
  8. theorem OAI.RegularPointCoordinates.sin_half_div_sin_ge_half line 110
  9. theorem OAI.RegularPointCoordinates.sinh_half_div_sinh line 122
  10. theorem OAI.RegularPointCoordinates.midpointFloor_le_sigma line 132
  11. theorem OAI.RegularPointCoordinates.midpointFloor_le_tau line 176
  12. theorem OAI.RegularPointCoordinates.geodesic_midpoint_mem_ball line 203
  13. def OAI.RegularPointCoordinates.ballGrowthConstant line 222
  14. theorem OAI.RegularPointCoordinates.ballGrowthConstant_pos line 225
  15. theorem OAI.RegularPointCoordinates.ballGrowthConstant_ne_top line 230
  16. theorem OAI.RegularPointCoordinates.FullCD.ball_growth line 236
  17. theorem OAI.RegularPointCoordinates.FullCD.ball_growth_iterated line 283
  18. theorem OAI.RegularPointCoordinates.FullCD.uniform_ball_volume_lower_bound line 313
  19. theorem OAI.RegularPointCoordinates.compact_closedBall_of_uniform_volume_lower_bound line 347
  20. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.proper line 390