OAI/Geometry/Arnold/Degeneracy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArnoldCounterexample.Construction.rotation_finish_neg line 14
2. lemma OAI.ArnoldCounterexample.Construction.forwardMid_zeroVector line 22
3. lemma OAI.ArnoldCounterexample.Construction.forwardMid_kernel line 25
4. def OAI.ArnoldCounterexample.Construction.degenerateLift line 31

   Source documentation

   Fix the phase of the lift at the degenerate point.

   def degenerateLift (w : CV) : CV := -forward (1,w)

   Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.Construction.forward

5. lemma OAI.ArnoldCounterexample.Construction.degenerateLift_smooth line 33
6. lemma OAI.ArnoldCounterexample.Construction.degenerateLift_zeroVector line 36
7. lemma OAI.ArnoldCounterexample.Construction.degenerateLift_preserves line 39
8. lemma OAI.ArnoldCounterexample.Construction.degenerateLift_project line 48
9. lemma OAI.ArnoldCounterexample.Construction.degenerateLift_kernel line 54
10. lemma OAI.ArnoldCounterexample.Construction.main_degenerate line 65