OAI/Geometry/Symplectic/MorseBounds/SymplecticFlow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MorseArnold.SymplecticFlow.TwoForm line 16
2. lemma OAI.MorseArnold.SymplecticFlow.alternating_skew line 18
3. lemma OAI.MorseArnold.SymplecticFlow.derivative_alt line 24
4. theorem OAI.MorseArnold.SymplecticFlow.infinitesimal_preservation line 36
5. lemma OAI.MorseArnold.SymplecticFlow.variational_derivative line 67
6. lemma OAI.MorseArnold.SymplecticFlow.derivative_altAt line 113
7. theorem OAI.MorseArnold.SymplecticFlow.infinitesimal_preservationAt line 127
8. lemma OAI.MorseArnold.SymplecticFlow.variational_derivativeAt line 156
9. lemma OAI.MorseArnold.SymplecticFlow.pullback_derivative_zeroAt line 201
10. theorem OAI.MorseArnold.SymplecticFlow.hamiltonian_flow_preserves_form line 227