OAI/Geometry/Symplectic/MorseBounds/CapForm.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MorseArnold.CapSymplectic.SI line 15
2. abbrev OAI.MorseArnold.CapSymplectic.PI line 16
3. def OAI.MorseArnold.CapSymplectic.planeArea line 17
4. def OAI.MorseArnold.CapSymplectic.fourPlaneForm line 20
5. def OAI.MorseArnold.CapSymplectic.fourSphereForm line 23
6. def OAI.MorseArnold.CapSymplectic.allChart line 27
7. def OAI.MorseArnold.CapSymplectic.CapSymplecticObligation line 31
8. lemma OAI.MorseArnold.CapSymplectic.planeArea_apply line 58
9. lemma OAI.MorseArnold.CapSymplectic.plane_chart line 61
10. lemma OAI.MorseArnold.CapSymplectic.plane_symplectic line 74
11. lemma OAI.MorseArnold.CapSymplectic.inclusion_inverse_deriv line 97
12. lemma OAI.MorseArnold.CapSymplectic.bigChart_inverse_area line 108
13. lemma OAI.MorseArnold.CapSymplectic.bigChart_area line 153
14. lemma OAI.MorseArnold.CapSymplectic.oneChart_area line 177
15. lemma OAI.MorseArnold.CapSymplectic.prod_area line 202
16. lemma OAI.MorseArnold.CapSymplectic.oneChart_mdiff line 222
17. lemma OAI.MorseArnold.CapSymplectic.pairChart_area line 228
18. lemma OAI.MorseArnold.CapSymplectic.fourChart_area line 244
19. lemma OAI.MorseArnold.CapSymplectic.allChart_area line 266
20. theorem OAI.MorseArnold.CapSymplectic.capSymplecticObligation line 289