OAI/Analysis/RCDHeat/VolumeComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: VolumeComparison, VolumeComparison, RatioComparison, VolumeComparison, VolumeComparison, VolumeComparison.

  1. theorem OAI.RegularPointCoordinates.sin_mul_div_sin_ge line 19
  2. theorem OAI.RegularPointCoordinates.sinh_le_mul_exp line 29
  3. theorem OAI.RegularPointCoordinates.sinh_mul_div_sinh_ge line 39
  4. def OAI.RegularPointCoordinates.distortionFloor line 52
  5. theorem OAI.RegularPointCoordinates.distortionFloor_le_time line 55
  6. theorem OAI.RegularPointCoordinates.distortionFloor_le_sigma line 61
  7. theorem OAI.RegularPointCoordinates.distortionFloor_le_tau line 94
  8. theorem OAI.RegularPointCoordinates.FullCD.ball_ratio_at_time line 124
  9. theorem OAI.RegularPointCoordinates.FullCD.ball_ratio line 185
  10. theorem OAI.RegularPointCoordinates.FullCD.flat_ball_ratio line 206
  11. theorem OAI.RegularPointCoordinates.FullCD.locDoubling line 221
  12. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.locDoubling line 246
  13. theorem OAI.RegularPointCoordinates.ediam_le_of_subset_closedBall line 259
  14. theorem OAI.RegularPointCoordinates.hausdorff_le_mul_measure_of_vitali line 271
  15. theorem OAI.RegularPointCoordinates.volume_coefficient_le_of_ball_cost line 326