OAI/Analysis/RCDHeat/KantorovichRadius.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: KantorovichRadius, KantorovichLeftLimit, KantorovichRelaxed, KantorovichGradient, KantorovichIdentity.

  1. theorem OAI.RegularPointCoordinates.hopf_minimizer_distance_mono line 21
  2. theorem OAI.RegularPointCoordinates.hopfRadius_le_later_minimizer line 47
  3. theorem OAI.RegularPointCoordinates.hopfRadius_monotone_time line 54
  4. theorem OAI.RegularPointCoordinates.hopfRadius_measurable line 65
  5. def OAI.RegularPointCoordinates.hopfLeftTime line 81
  6. theorem OAI.RegularPointCoordinates.hopfLeftTime_bounds line 82
  7. theorem OAI.RegularPointCoordinates.hopfLeftTime_pos line 88
  8. theorem OAI.RegularPointCoordinates.hopfLeftTime_mono line 89
  9. theorem OAI.RegularPointCoordinates.hopfLeftTime_tendsto line 94
  10. def OAI.RegularPointCoordinates.hopfLeftRadius line 107
  11. theorem OAI.RegularPointCoordinates.hopfLeftRadius_bdd line 110
  12. theorem OAI.RegularPointCoordinates.hopfLeftRadius_bounds line 118
  13. theorem OAI.RegularPointCoordinates.hopfLeftRadius_tendsto line 128
  14. theorem OAI.RegularPointCoordinates.hopfLeftRadius_le_minimizer line 135
  15. theorem OAI.RegularPointCoordinates.hopfLeftRadius_measurable line 142
  16. theorem OAI.RegularPointCoordinates.hopfLeftRadius_memLp line 156
  17. theorem OAI.RegularPointCoordinates.hopfScaledRadius_bounds line 161
  18. theorem OAI.RegularPointCoordinates.hopfScaledRadius_memLp line 169
  19. theorem OAI.RegularPointCoordinates.hopfScaledRadius_toLp_tendsto line 174
  20. theorem OAI.RegularPointCoordinates.hopfLeft_toLp_tendsto line 190
  21. theorem OAI.RegularPointCoordinates.hopfLeftRadius_isRelaxed line 219
  22. theorem OAI.RegularPointCoordinates.hopfLeftRadius_minimalSlope_bound line 247
  23. theorem OAI.RegularPointCoordinates.hopfLax_of_contact line 268
  24. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.compact_sobolev_potential line 288
  25. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.kantorovich_gradient_eq_displacement line 330
  26. theorem OAI.RegularPointCoordinates.compact_optimal_plan_gradient_identity line 365