OAI/Geometry/Symplectic/MorseBounds/CotangentFlow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MorseArnold.GenericGeometry.chart_inverse_derivative line 17
2. lemma OAI.MorseArnold.GenericGeometry.chartTwoForm_apply_derivatives line 28
3. lemma OAI.MorseArnold.GenericGeometry.coordinate_flow_smooth_at line 46
4. lemma OAI.MorseArnold.GenericGeometry.coordinate_derivative_apply line 69
5. lemma OAI.MorseArnold.GenericGeometry.chart_function_smooth line 106
6. lemma OAI.MorseArnold.GenericGeometry.manifold_pullback_derivative_zero line 115
7. theorem OAI.MorseArnold.GenericGeometry.manifold_hamiltonian_flow_preserves_form line 195