OAI/Analysis/RCDHeat/CompressionIntegral.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CompressionIntegral, TestPlanMajorant, TestPlanRelaxed, TestPlanAE, GeodesicSubpath, TestPlanSubinterval.

  1. theorem OAI.RegularPointCoordinates.compression_weighted_integral_continuous line 17
  2. theorem OAI.RegularPointCoordinates.lp_integral_norm_continuous line 31
  3. theorem OAI.RegularPointCoordinates.testPlan_slope_memLp line 55
  4. theorem OAI.RegularPointCoordinates.testPlan_length_memLp line 67
  5. theorem OAI.RegularPointCoordinates.testPlan_slope_majorized line 72
  6. theorem OAI.RegularPointCoordinates.lipschitz_testPlan_increment_le_majorant line 84
  7. theorem OAI.RegularPointCoordinates.testPlan_increment_continuous line 133
  8. theorem OAI.RegularPointCoordinates.testPlan_gradient_integral_continuous line 151
  9. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_increment line 164
  10. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_increment line 185
  11. def OAI.RegularPointCoordinates.timeSegment line 230
  12. theorem OAI.RegularPointCoordinates.timeSegment_zero line 239
  13. theorem OAI.RegularPointCoordinates.timeSegment_one line 242
  14. def OAI.RegularPointCoordinates.subpath line 246
  15. theorem OAI.RegularPointCoordinates.subpath_zero line 248
  16. theorem OAI.RegularPointCoordinates.subpath_one line 250
  17. theorem OAI.RegularPointCoordinates.subpath_continuous line 253
  18. theorem OAI.RegularPointCoordinates.IsGeodesic.subpath line 256
  19. theorem OAI.RegularPointCoordinates.subpath_measurable line 271
  20. theorem OAI.RegularPointCoordinates.subpath_map_eval line 274
  21. theorem OAI.RegularPointCoordinates.testPlan_subpath_length_memLp line 280
  22. theorem OAI.RegularPointCoordinates.subpath_extension line 297
  23. theorem OAI.RegularPointCoordinates.subpath_integral line 305
  24. theorem OAI.RegularPointCoordinates.isClosed_geodesicSet line 324
  25. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_subinterval line 338