OAI/Geometry/Symplectic/MorseBounds/SphereHamiltonian.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MorseArnold.SphereHamiltonian.ambientVelocity line 16
2. lemma OAI.MorseArnold.SphereHamiltonian.ambientVelocity_range line 20
3. def OAI.MorseArnold.SphereHamiltonian.velocity line 27
4. lemma OAI.MorseArnold.SphereHamiltonian.tangent_velocity line 30
5. lemma OAI.MorseArnold.SphereHamiltonian.vec3_time_deriv line 34
6. lemma OAI.MorseArnold.SphereHamiltonian.rotateAmbient_deriv line 46
7. lemma OAI.MorseArnold.SphereHamiltonian.sphereFlow_ambient_deriv line 59
8. lemma OAI.MorseArnold.SphereHamiltonian.sphereFlow_ode line 64
9. lemma OAI.MorseArnold.SphereHamiltonian.hamiltonian_differential line 96
10. theorem OAI.MorseArnold.SphereHamiltonian.sphere_hamiltonian_flow line 111