OAI/Geometry/Symplectic/MorseBounds/ProductForm.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MorseArnold.SymplecticProduct.TwoForm line 23
2. def OAI.MorseArnold.SymplecticProduct.chartTwoForm line 25
3. structure OAI.MorseArnold.SymplecticProduct.SymplecticForm line 31
4. def OAI.MorseArnold.SymplecticProduct.prodForm line 41
5. def OAI.MorseArnold.SymplecticProduct.ProductSymplecticExistence line 54
6. def OAI.MorseArnold.SymplecticProduct.pullBilin line 83
7. lemma OAI.MorseArnold.SymplecticProduct.pullBilin_apply line 89
8. lemma OAI.MorseArnold.SymplecticProduct.chartTwoForm_apply line 93
9. lemma OAI.MorseArnold.SymplecticProduct.prodForm_apply line 99
10. lemma OAI.MorseArnold.SymplecticProduct.chart_prod_derivative line 103
11. lemma OAI.MorseArnold.SymplecticProduct.chart_prod line 122
12. lemma OAI.MorseArnold.SymplecticProduct.prod_alternating line 141
13. lemma OAI.MorseArnold.SymplecticProduct.prod_nondegenerate line 149
14. lemma OAI.MorseArnold.SymplecticProduct.chart_prod_eventually line 166
15. lemma OAI.MorseArnold.SymplecticProduct.prod_chart_smooth line 179
16. lemma OAI.MorseArnold.SymplecticProduct.prod_chart_deriv line 214
17. lemma OAI.MorseArnold.SymplecticProduct.prod_closed line 234
18. def OAI.MorseArnold.SymplecticProduct.symplecticProd line 252
19. theorem OAI.MorseArnold.SymplecticProduct.productSymplecticExistence line 260