OAI/Geometry/Symplectic/MorseBounds/Periodization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MorseArnold.Periodization.rho line 14
  2. def OAI.MorseArnold.Periodization.periodicHamiltonian line 16
  3. def OAI.MorseArnold.Periodization.periodizedFlow line 23
  4. def OAI.MorseArnold.Periodization.periodizedVector line 26
  5. lemma OAI.MorseArnold.Periodization.rho_smooth line 29
  6. lemma OAI.MorseArnold.Periodization.rho_deriv_smooth line 32
  7. lemma OAI.MorseArnold.Periodization.rho_zero line 34
  8. lemma OAI.MorseArnold.Periodization.rho_one line 38
  9. lemma OAI.MorseArnold.Periodization.rho_deriv_zero line 42
  10. lemma OAI.MorseArnold.Periodization.floor_on_cell line 53
  11. lemma OAI.MorseArnold.Periodization.fract_on_cell line 56
  12. lemma OAI.MorseArnold.Periodization.floor_near_seam line 59
  13. lemma OAI.MorseArnold.Periodization.hamiltonian_near_seam line 71
  14. lemma OAI.MorseArnold.Periodization.flow_near_seam line 79
  15. lemma OAI.MorseArnold.Periodization.endpoint_power_smooth line 90
  16. theorem OAI.MorseArnold.Periodization.periodicHamiltonian_smooth line 99
  17. theorem OAI.MorseArnold.Periodization.periodicHamiltonian_periodic line 124
  18. theorem OAI.MorseArnold.Periodization.periodizedFlow_smooth line 128
  19. theorem OAI.MorseArnold.Periodization.periodizedFlow_endpoints line 159
  20. lemma OAI.MorseArnold.Periodization.reparam_ode line 166
  21. theorem OAI.MorseArnold.Periodization.periodizedFlow_ode line 190
  22. theorem OAI.MorseArnold.Periodization.periodizedVector_hamiltonian line 233