OAI/Geometry/Symplectic/MorseBounds/Dynamics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MorseArnold.Dynamics.exp_sub_one_isUnit_small line 13
2. theorem OAI.MorseArnold.Dynamics.exp_sub_one_isUnit_small_finite line 43
3. theorem OAI.MorseArnold.Dynamics.short_loop_constant line 60
4. def OAI.MorseArnold.Dynamics.coordinateVectorField line 132
5. theorem OAI.MorseArnold.Dynamics.coordinateVectorField_contDiffAt line 138
6. theorem OAI.MorseArnold.Dynamics.coordinateVectorField_apply line 147
7. theorem OAI.MorseArnold.Dynamics.integralCurve_coordinate_derivative line 156
8. theorem OAI.MorseArnold.Dynamics.coordinateVectorField_eq_zero_iff line 176
9. theorem OAI.MorseArnold.Dynamics.local_short_period line 190
10. theorem OAI.MorseArnold.Dynamics.compact_short_period line 242
11. theorem OAI.MorseArnold.Dynamics.coordinate_flow_smooth line 292
12. theorem OAI.MorseArnold.Dynamics.manifold_small_time_nondegenerate line 312