OAI/Analysis/RCDHeat/MetricUpperGradient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: MetricUpperGradient, HeatLength, CountableMetricSpeed, MetricSpeedPointwise, MetricTwoSidedSpeed, HeatTwoSidedSpeed.

  1. theorem OAI.RegularPointCoordinates.dist_le_integral_of_ae_right_speed line 17
  2. theorem OAI.RegularPointCoordinates.intervalIntegrable_sqrt_nonneg line 49
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_fisher_length line 62
  4. def OAI.RegularPointCoordinates.countableMetricSpeed line 116
  5. theorem OAI.RegularPointCoordinates.countableMetricSpeed_measurable line 118
  6. theorem OAI.RegularPointCoordinates.countableMetricSpeed_deriv_le line 120
  7. theorem OAI.RegularPointCoordinates.ac_distance_test line 126
  8. theorem OAI.RegularPointCoordinates.countableMetricSpeed_ae_le line 131
  9. theorem OAI.RegularPointCoordinates.countableMetricSpeed_intervalIntegrable line 152
  10. theorem OAI.RegularPointCoordinates.scalar_distance_le_integral_countableMetricSpeed line 165
  11. theorem OAI.RegularPointCoordinates.dist_le_of_rat_distance_test line 178
  12. theorem OAI.RegularPointCoordinates.dist_le_integral_countableMetricSpeed line 192
  13. theorem OAI.RegularPointCoordinates.tendsto_metric_quotient_of_envelope line 218
  14. theorem OAI.RegularPointCoordinates.dist_le_abs_countableSpeed_primitive line 254
  15. theorem OAI.RegularPointCoordinates.ae_metric_speed_of_right_speed line 281
  16. theorem OAI.RegularPointCoordinates.ae_metric_derivative_of_right_speed line 314
  17. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_probability_metric_speed line 331