OAI/Analysis/RCDHeat/HopfHeat.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HopfHeat.

  1. def OAI.RegularPointCoordinates.hopfLax line 20
  2. theorem OAI.RegularPointCoordinates.hopfLax_cost_lower line 23
  3. theorem OAI.RegularPointCoordinates.hopfLax_bddBelow line 36
  4. theorem OAI.RegularPointCoordinates.hopfLax_le_cost line 43
  5. theorem OAI.RegularPointCoordinates.hopfLax_bounds line 48
  6. theorem OAI.RegularPointCoordinates.hopfLax_antitone_time line 56
  7. theorem OAI.RegularPointCoordinates.hopfLax_exists_minimizer line 66
  8. theorem OAI.RegularPointCoordinates.hopfLax_difference_upper line 101
  9. theorem OAI.RegularPointCoordinates.hopfLax_abs_difference line 123
  10. theorem OAI.RegularPointCoordinates.hopfLax_minimizer_dist line 132
  11. theorem OAI.RegularPointCoordinates.hopfLax_continuous line 145
  12. def OAI.RegularPointCoordinates.hopfMinimizers line 166
  13. theorem OAI.RegularPointCoordinates.hopfMinimizers_nonempty line 169
  14. theorem OAI.RegularPointCoordinates.hopfMinimizers_compact line 175
  15. def OAI.RegularPointCoordinates.hopfRadius line 186
  16. theorem OAI.RegularPointCoordinates.hopfRadius_attained line 189
  17. theorem OAI.RegularPointCoordinates.hopfRadius_bounds line 197
  18. theorem OAI.RegularPointCoordinates.dist_le_hopfRadius line 204
  19. theorem OAI.RegularPointCoordinates.hopfRadius_upperSemicontinuous line 215
  20. theorem OAI.RegularPointCoordinates.hopfLax_difference_radius line 256
  21. theorem OAI.RegularPointCoordinates.hopfLax_slope_le_eps line 277
  22. theorem OAI.RegularPointCoordinates.hopfLax_slope_le line 302
  23. theorem OAI.RegularPointCoordinates.hopfLax_time_derivative line 315
  24. theorem OAI.RegularPointCoordinates.hopfLax_hamiltonJacobi line 336
  25. theorem OAI.RegularPointCoordinates.hopfLax_minimizer_dist_sharp line 351
  26. theorem OAI.RegularPointCoordinates.hopfRadius_le_sharp line 396
  27. theorem OAI.RegularPointCoordinates.hopfLax_slope_le_lipschitz line 403
  28. theorem OAI.RegularPointCoordinates.lipschitz_of_quadratic_cost line 412
  29. theorem OAI.RegularPointCoordinates.hopfLax_lipschitz line 473
  30. lemma OAI.RegularPointCoordinates.quadratic_weighted_triangle line 488
  31. theorem OAI.RegularPointCoordinates.hopfLax_semigroup line 499
  32. theorem OAI.RegularPointCoordinates.hopfLax_time_difference_sharp line 546
  33. theorem OAI.RegularPointCoordinates.hopfLax_tendsto_zero line 571