OAI/Analysis/RCDHeat/EntropyPlanExtension.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EntropyPlanExtension, LastMeeting, GeodesicSplice, CrossingGeometry, BoundedDensityLp.

  1. def OAI.RegularPointCoordinates.entropyPlanExtension line 18
  2. lemma OAI.RegularPointCoordinates.entropyPlanExtension_eq line 22
  3. def OAI.RegularPointCoordinates.lastMeeting line 38
  4. lemma OAI.RegularPointCoordinates.lastMeeting_mem line 42
  5. lemma OAI.RegularPointCoordinates.lastMeeting_le line 49
  6. lemma OAI.RegularPointCoordinates.lastMeeting_eq line 55
  7. lemma OAI.RegularPointCoordinates.le_lastMeeting line 62
  8. lemma OAI.RegularPointCoordinates.ne_after_lastMeeting line 67
  9. lemma OAI.RegularPointCoordinates.measurable_lastMeeting line 73
  10. def OAI.RegularPointCoordinates.spliceAt line 93
  11. lemma OAI.RegularPointCoordinates.spliceAt_apply line 99
  12. def OAI.RegularPointCoordinates.lastMeetingSplice line 104
  13. lemma OAI.RegularPointCoordinates.measurable_path_of_eval line 109
  14. lemma OAI.RegularPointCoordinates.measurable_lastMeetingSplice line 122
  15. lemma OAI.RegularPointCoordinates.isGeodesic_of_upper line 155
  16. lemma OAI.RegularPointCoordinates.spliceAt_zero line 174
  17. lemma OAI.RegularPointCoordinates.spliceAt_one line 179
  18. lemma OAI.RegularPointCoordinates.geodesic_speeds_equal_of_initial_segment line 188
  19. lemma OAI.RegularPointCoordinates.isGeodesic_spliceAt line 198
  20. lemma OAI.RegularPointCoordinates.lastMeetingSplice_properties line 229
  21. lemma OAI.RegularPointCoordinates.weighted_square_equality line 261
  22. def OAI.RegularPointCoordinates.crossingSplice line 276
  23. lemma OAI.RegularPointCoordinates.crossingSplice_apply line 281
  24. lemma OAI.RegularPointCoordinates.measurable_crossingSplice line 287
  25. lemma OAI.RegularPointCoordinates.isGeodesic_spliceAt_of_cross_length line 307
  26. lemma OAI.RegularPointCoordinates.crossing_geodesic_distance_bound line 340
  27. theorem OAI.RegularPointCoordinates.bounded_density_lp_realization line 358