OAI/Geometry/Symplectic/MorseBounds/ManifoldFlow.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MorseArnold.ManifoldFlow.smooth_extension_near line 17
2. lemma OAI.MorseArnold.ManifoldFlow.exists_local_smooth_flow_on line 38
3. def OAI.MorseArnold.ManifoldFlow.chartField line 81
4. lemma OAI.MorseArnold.ManifoldFlow.chartField_smooth line 86
5. lemma OAI.MorseArnold.ManifoldFlow.chart_integralCurve line 107
6. theorem OAI.MorseArnold.ManifoldFlow.exists_local_smooth_manifold_flow line 129
7. lemma OAI.MorseArnold.ManifoldFlow.compact_uniform_time line 169
8. theorem OAI.MorseArnold.ManifoldFlow.exists_global_integral_curves line 188
9. theorem OAI.MorseArnold.ManifoldFlow.flow_law_of_integral_curves line 202
10. lemma OAI.MorseArnold.ManifoldFlow.uniform_smooth_near_zero line 214
11. lemma OAI.MorseArnold.ManifoldFlow.flow_nat_mul line 239
12. lemma OAI.MorseArnold.ManifoldFlow.smooth_of_uniform_short_time line 249
13. theorem OAI.MorseArnold.ManifoldFlow.exists_compact_smooth_flow line 280
14. def OAI.MorseArnold.ManifoldFlow.CompactSmoothFlowExistence line 301
15. theorem OAI.MorseArnold.ManifoldFlow.compactSmoothFlowExistence line 317
16. lemma OAI.MorseArnold.ManifoldFlow.compact_core_uniform_time line 331
17. theorem OAI.MorseArnold.ManifoldFlow.exists_core_global_integral_curves line 350
18. lemma OAI.MorseArnold.ManifoldFlow.core_uniform_smooth_near_zero line 369
19. theorem OAI.MorseArnold.ManifoldFlow.exists_compact_core_smooth_flow line 408
20. def OAI.MorseArnold.ManifoldFlow.CompactCoreSmoothFlowExistence line 438
21. theorem OAI.MorseArnold.ManifoldFlow.compactCoreSmoothFlowExistence line 463