OAI/Geometry/PolarProducts/ExteriorHamiltonian.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PushedBall.domain line 16
  2. def OAI.PushedBall.core line 17
  3. def OAI.PushedBall.radial line 18
  4. theorem OAI.PushedBall.isOpen_domain line 20
  5. theorem OAI.PushedBall.core_compact line 23
  6. theorem OAI.PushedBall.mem_core_iff line 25
  7. theorem OAI.PushedBall.core_subset_domain line 30
  8. theorem OAI.PushedBall.contDiff_radial line 37
  9. theorem OAI.PushedBall.radial_eq_height line 40
  10. def OAI.PushedBall.pushed line 45
  11. theorem OAI.PushedBall.contDiff_pushed line 48
  12. theorem OAI.PushedBall.pushed_apply line 58
  13. theorem OAI.PushedBall.pushed_plateau line 62
  14. theorem OAI.PushedBall.pushed_bounds line 68
  15. theorem OAI.PushedBall.zero_mem_domain line 77
  16. theorem OAI.PushedBall.radial_flat line 80
  17. theorem OAI.PushedBall.pushed_flat line 87
  18. theorem OAI.PushedBall.radial_slow line 97
  19. def OAI.ExteriorHamiltonian.potential line 114
  20. def OAI.ExteriorHamiltonian.full line 115
  21. theorem OAI.ExteriorHamiltonian.contDiff_potential line 118
  22. theorem OAI.ExteriorHamiltonian.contDiff_full line 121
  23. theorem OAI.ExteriorHamiltonian.gradient_potential line 124
  24. theorem OAI.ExteriorHamiltonian.gradient_sum line 131
  25. theorem OAI.ExteriorHamiltonian.gradient_full line 143
  26. theorem OAI.ExteriorHamiltonian.gradient_at_max line 149
  27. theorem OAI.ExteriorHamiltonian.gradient_at_min line 154
  28. theorem OAI.ExteriorHamiltonian.potential_zero line 159
  29. theorem OAI.ExteriorHamiltonian.potential_nonneg line 162
  30. theorem OAI.ExteriorHamiltonian.compact_sublevel line 165
  31. theorem OAI.ExteriorHamiltonian.bounded_remainder line 177
  32. theorem OAI.ExteriorHamiltonian.full_flat line 191
  33. theorem OAI.ExteriorHamiltonian.action_nonpos line 209
  34. theorem OAI.ExteriorHamiltonian.gradient_of_constant_curve line 215
  35. theorem OAI.ExteriorHamiltonian.action_nonpos_of_constant line 224
  36. theorem OAI.ExteriorHamiltonian.high_orbit_nonpos line 232
  37. theorem OAI.ExteriorHamiltonian.zero_vector_at_plateau line 274
  38. theorem OAI.ExteriorHamiltonian.all_orbits_nonpos line 290
  39. theorem OAI.PushedBall.pushed_full_comp line 339
  40. theorem OAI.PushedBall.pushed_full_slow line 345
  41. theorem OAI.PushedBall.pushed_plateau_outside line 362