OAI/Analysis/RCDHeat/TestPlanContinuous.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: TestPlanContinuous, TestPlanDerivative, DenseACExtension, TestPlanClock, TestPlanRepresentative.

  1. theorem OAI.RegularPointCoordinates.testPlan_eval_intervalIntegrable line 19
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_distance line 30
  3. def OAI.RegularPointCoordinates.rationalTime line 47
  4. theorem OAI.RegularPointCoordinates.rationalTime_dense line 48
  5. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_absolutelyContinuous line 54
  6. theorem OAI.RegularPointCoordinates.abs_deriv_le_of_dist_domination line 118
  7. theorem OAI.RegularPointCoordinates.testPlan_eval_nonneg line 133
  8. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_derivative line 145
  9. theorem OAI.RegularPointCoordinates.exists_continuous_extension_of_rat_control line 194
  10. def OAI.RegularPointCoordinates.testPlanPrimitive line 227
  11. theorem OAI.RegularPointCoordinates.testPlanPrimitive_measurable line 231
  12. theorem OAI.RegularPointCoordinates.testPlanPrimitive_uniformContinuous line 255
  13. theorem OAI.RegularPointCoordinates.testPlanPrimitive_dist line 264
  14. def OAI.RegularPointCoordinates.testPlanClock line 276
  15. theorem OAI.RegularPointCoordinates.testPlanClock_measurable line 280
  16. theorem OAI.RegularPointCoordinates.testPlanClock_uniformContinuous line 286
  17. theorem OAI.RegularPointCoordinates.testPlanClock_dist line 292
  18. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_clock_rat line 309
  19. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_representative line 349