OAI/Geometry/Symplectic/MorseBounds/Cotangent.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MorseArnold.GenericGeometry.SmoothModel line 14
  2. abbrev OAI.MorseArnold.GenericGeometry.TwoForm line 19
  3. def OAI.MorseArnold.GenericGeometry.chartTwoForm line 22
  4. structure OAI.MorseArnold.GenericGeometry.SymplecticForm line 29
  5. def OAI.MorseArnold.GenericGeometry.criticalSet line 41
  6. def OAI.MorseArnold.GenericGeometry.IsMorse line 44
  7. def OAI.MorseArnold.GenericGeometry.morseCounts line 51
  8. def OAI.MorseArnold.GenericGeometry.ordinaryMorseNumber line 54
  9. lemma OAI.MorseArnold.GenericGeometry.inverse_chart_coordinateVectorField line 68
  10. lemma OAI.MorseArnold.GenericGeometry.chart_hamiltonian_equation line 87
  11. lemma OAI.MorseArnold.GenericGeometry.chartTwoForm_nondegenerate line 114
  12. theorem OAI.MorseArnold.GenericGeometry.hamiltonian_field_coordinate_isUnit line 129
  13. theorem OAI.MorseArnold.GenericGeometry.hamiltonian_small_time_nondegenerate line 171
  14. lemma OAI.MorseArnold.GenericGeometry.hamiltonian_zero_iff_critical line 229
  15. lemma OAI.MorseArnold.GenericGeometry.hamiltonian_criticalSet_closed line 251
  16. lemma OAI.MorseArnold.GenericGeometry.hamiltonian_criticalSet_discrete line 279
  17. theorem OAI.MorseArnold.GenericGeometry.hamiltonian_criticalSet_finite line 322
  18. theorem OAI.MorseArnold.GenericGeometry.compact_hamiltonian_small_time line 333
  19. lemma OAI.MorseArnold.GenericGeometry.bilinear_invertible line 407
  20. def OAI.MorseArnold.GenericGeometry.hamiltonianField line 420
  21. lemma OAI.MorseArnold.GenericGeometry.hamiltonianField_equation line 426
  22. lemma OAI.MorseArnold.GenericGeometry.hamiltonianField_coordinate_smooth line 433
  23. lemma OAI.MorseArnold.GenericGeometry.hamiltonianField_smooth line 459
  24. theorem OAI.MorseArnold.GenericGeometry.exists_smooth_hamiltonian_field line 474
  25. def OAI.MorseArnold.GenericGeometry.LocalHamiltonianModelExistence line 490
  26. lemma OAI.MorseArnold.GenericGeometry.flow_core_invariant line 526
  27. lemma OAI.MorseArnold.GenericGeometry.criticalSet_subset_core line 537
  28. theorem OAI.MorseArnold.GenericGeometry.localHamiltonianModelExistence line 554