OAI/Geometry/Symplectic/MorseBounds/SphereSmooth.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MorseArnold.SphereCaps.capHeight line 15
  2. def OAI.MorseArnold.SphereCaps.capStep line 16
  3. def OAI.MorseArnold.SphereCaps.angularSpeed line 17
  4. def OAI.MorseArnold.SphereCaps.rotateAmbient line 21
  5. def OAI.MorseArnold.SphereCaps.rotatePlane line 24
  6. lemma OAI.MorseArnold.SphereCaps.rotateAmbient_height line 27
  7. lemma OAI.MorseArnold.SphereCaps.rotateAmbient_sq line 29
  8. theorem OAI.MorseArnold.SphereCaps.rotate_mem line 37
  9. def OAI.MorseArnold.SphereCaps.rotate line 46
  10. def OAI.MorseArnold.SphereCaps.sphereFlow line 47
  11. def OAI.MorseArnold.SphereCaps.poleSet line 50
  12. def OAI.MorseArnold.SphereCaps.sphereHamiltonian line 51
  13. lemma OAI.MorseArnold.SphereCaps.capStep_smooth line 54
  14. lemma OAI.MorseArnold.SphereCaps.angularSpeed_smooth line 57
  15. lemma OAI.MorseArnold.SphereCaps.angularSpeed_bounds line 61
  16. lemma OAI.MorseArnold.SphereCaps.capHeight_pos line 68
  17. lemma OAI.MorseArnold.SphereCaps.capStep_north line 74
  18. lemma OAI.MorseArnold.SphereCaps.capStep_south line 80
  19. theorem OAI.MorseArnold.SphereCaps.speed_properties line 86
  20. lemma OAI.MorseArnold.SphereCaps.rotateAmbient_zero line 104
  21. lemma OAI.MorseArnold.SphereCaps.rotateAmbient_add line 108
  22. lemma OAI.MorseArnold.SphereCaps.rotate_zero line 113
  23. lemma OAI.MorseArnold.SphereCaps.rotate_add line 117
  24. lemma OAI.MorseArnold.SphereCaps.rotate_height line 121
  25. theorem OAI.MorseArnold.SphereCaps.sphereFlow_laws line 123
  26. lemma OAI.MorseArnold.SphereCaps.rotateAmbient_smooth line 132
  27. lemma OAI.MorseArnold.SphereCaps.rotate_smooth line 143
  28. lemma OAI.MorseArnold.SphereCaps.height_smooth line 154
  29. lemma OAI.MorseArnold.SphereCaps.sphereFlow_time_smooth line 159
  30. theorem OAI.MorseArnold.SphereCaps.sphereFlow_smooth line 169
  31. lemma OAI.MorseArnold.SphereCaps.rotate_fixed_iff line 179
  32. theorem OAI.MorseArnold.SphereCaps.sphereFlow_fixed line 203
  33. lemma OAI.MorseArnold.SphereCaps.north_rotate line 210
  34. lemma OAI.MorseArnold.SphereCaps.south_rotate line 214
  35. lemma OAI.MorseArnold.SphereCaps.rotatePlane_two_pi_sub line 218
  36. lemma OAI.MorseArnold.SphereCaps.rotatePlane_neg_two_pi_sub line 222
  37. lemma OAI.MorseArnold.SphereCaps.north_cap_height line 226
  38. lemma OAI.MorseArnold.SphereCaps.south_cap_height line 236
  39. theorem OAI.MorseArnold.SphereCaps.sphereFlow_north_endpoint line 246
  40. theorem OAI.MorseArnold.SphereCaps.sphereFlow_south_endpoint line 260
  41. lemma OAI.MorseArnold.SphereCaps.sphereHamiltonian_deriv line 273
  42. lemma OAI.MorseArnold.SphereCaps.sphereHamiltonian_smooth line 279
  43. theorem OAI.MorseArnold.SphereCaps.sphere_hamiltonian_equation line 287