OAI/Geometry/WeakHessian/Transport/HopfObjective.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessianTransport.hopfObjective line 30
  2. def OAI.WeakHessianTransport.hopfLax line 33
  3. lemma OAI.WeakHessianTransport.hopfObjective_bddBelow line 36
  4. lemma OAI.WeakHessianTransport.hopfLax_le_objective line 43
  5. lemma OAI.WeakHessianTransport.hopfLax_le_self line 48
  6. lemma OAI.WeakHessianTransport.lower_le_hopfLax line 53
  7. lemma OAI.WeakHessianTransport.continuous_hopfObjective line 59
  8. lemma OAI.WeakHessianTransport.hopfLax_mono_function line 64
  9. lemma OAI.WeakHessianTransport.hopfLax_antitone_time line 71
  10. lemma OAI.WeakHessianTransport.exists_hopf_minimizer line 80
  11. lemma OAI.WeakHessianTransport.hopf_minimizer_distance_sq line 112
  12. lemma OAI.WeakHessianTransport.hopf_spatial_increment line 124
  13. lemma OAI.WeakHessianTransport.hopf_minimizer_distance_le line 146
  14. lemma OAI.WeakHessianTransport.hopf_spatial_abs_increment line 154
  15. lemma OAI.WeakHessianTransport.hopfLax_lipschitz_radius line 169
  16. lemma OAI.WeakHessianTransport.hopfLax_continuous line 192
  17. lemma OAI.WeakHessianTransport.hopf_time_increment line 198
  18. lemma OAI.WeakHessianTransport.hopf_time_increment_bound line 209
  19. lemma OAI.WeakHessianTransport.hopf_time_abs_bound line 222
  20. lemma OAI.WeakHessianTransport.hopfLax_time_continuousAt line 238
  21. lemma OAI.WeakHessianTransport.hopfLax_ge_lipschitz line 250
  22. lemma OAI.WeakHessianTransport.hopf_minimizer_distance_lipschitz line 265
  23. def OAI.WeakHessianTransport.IsFarthestHopfMinimizer line 284
  24. lemma OAI.WeakHessianTransport.hopf_minimizers_compact line 288
  25. lemma OAI.WeakHessianTransport.exists_farthest_hopf_minimizer line 300
  26. lemma OAI.WeakHessianTransport.eventually_hopf_minimizer_distance_lt line 307
  27. lemma OAI.WeakHessianTransport.hopf_time_derivative_at_minimizer line 344
  28. lemma OAI.WeakHessianTransport.hopf_spatial_quotient_bound line 364
  29. lemma OAI.WeakHessianTransport.hopf_localSlope_le line 381
  30. lemma OAI.WeakHessianTransport.hopf_hamiltonJacobi_at line 415
  31. lemma OAI.WeakHessianTransport.hopf_hamiltonJacobi_ae line 430