OAI/Geometry/Symplectic/MorseBounds/Ambient.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MorseArnold.AmbientHamiltonian.SI line 16
  2. abbrev OAI.MorseArnold.AmbientHamiltonian.AI line 17
  3. def OAI.MorseArnold.AmbientHamiltonian.onePotential line 19
  4. def OAI.MorseArnold.AmbientHamiltonian.pairPotential line 21
  5. def OAI.MorseArnold.AmbientHamiltonian.fourPotential line 23
  6. def OAI.MorseArnold.AmbientHamiltonian.pairVelocity line 26
  7. def OAI.MorseArnold.AmbientHamiltonian.fourVelocity line 28
  8. def OAI.MorseArnold.AmbientHamiltonian.areaValue line 30
  9. def OAI.MorseArnold.AmbientHamiltonian.ambientPotential line 35
  10. def OAI.MorseArnold.AmbientHamiltonian.ambientFlow line 36
  11. def OAI.MorseArnold.AmbientHamiltonian.ambientVelocity line 38
  12. def OAI.MorseArnold.AmbientHamiltonian.AmbientHamiltonianObligation line 41
  13. def OAI.MorseArnold.AmbientHamiltonian.promote line 72
  14. lemma OAI.MorseArnold.AmbientHamiltonian.prod_potential_deriv line 87
  15. lemma OAI.MorseArnold.AmbientHamiltonian.prod_hamiltonian line 97
  16. lemma OAI.MorseArnold.AmbientHamiltonian.prod_curve_ode line 111
  17. lemma OAI.MorseArnold.AmbientHamiltonian.smooth_id_flow line 124
  18. lemma OAI.MorseArnold.AmbientHamiltonian.onePotential_smooth line 136
  19. lemma OAI.MorseArnold.AmbientHamiltonian.pairPotential_smooth line 138
  20. lemma OAI.MorseArnold.AmbientHamiltonian.fourPotential_smooth line 141
  21. lemma OAI.MorseArnold.AmbientHamiltonian.four_flow_ode line 145
  22. lemma OAI.MorseArnold.AmbientHamiltonian.one_hamiltonian line 152
  23. lemma OAI.MorseArnold.AmbientHamiltonian.ambient_hamiltonian_eq line 168
  24. lemma OAI.MorseArnold.AmbientHamiltonian.ambientFlow_smooth line 186
  25. lemma OAI.MorseArnold.AmbientHamiltonian.ambient_flow_laws line 192
  26. lemma OAI.MorseArnold.AmbientHamiltonian.ambient_flow_ode line 205
  27. lemma OAI.MorseArnold.AmbientHamiltonian.ambient_fixed line 214
  28. theorem OAI.MorseArnold.AmbientHamiltonian.ambientHamiltonianObligation line 220