OAI/Geometry/Symplectic/MorseBounds/SmoothODE.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MorseArnold.SmoothODE.superposition line 19
  2. def OAI.MorseArnold.SmoothODE.pathLinear line 22
  3. theorem OAI.MorseArnold.SmoothODE.pathLinear_apply line 35
  4. def OAI.MorseArnold.SmoothODE.pathLinearCLM line 38
  5. theorem OAI.MorseArnold.SmoothODE.uniform_taylor line 52
  6. theorem OAI.MorseArnold.SmoothODE.hasFDerivAt_superposition line 83
  7. theorem OAI.MorseArnold.SmoothODE.contDiff_superposition_nat line 100
  8. theorem OAI.MorseArnold.SmoothODE.contDiff_superposition line 115
  9. abbrev OAI.MorseArnold.SmoothODE.J line 121
  10. def OAI.MorseArnold.SmoothODE.PathSpace line 123
  11. def OAI.MorseArnold.SmoothODE.extendPath line 127
  12. theorem OAI.MorseArnold.SmoothODE.continuous_extendPath line 130
  13. def OAI.MorseArnold.SmoothODE.primitive line 133
  14. theorem OAI.MorseArnold.SmoothODE.primitive_apply line 139
  15. def OAI.MorseArnold.SmoothODE.primitiveCLM line 142
  16. theorem OAI.MorseArnold.SmoothODE.primitiveCLM_apply line 167
  17. def OAI.MorseArnold.SmoothODE.constPathCLM line 169
  18. theorem OAI.MorseArnold.SmoothODE.constPathCLM_apply line 180
  19. def OAI.MorseArnold.SmoothODE.picardMap line 182
  20. theorem OAI.MorseArnold.SmoothODE.contDiff_picardMap line 187
  21. def OAI.MorseArnold.SmoothODE.picardLinearEquiv line 195
  22. theorem OAI.MorseArnold.SmoothODE.hasFDerivAt_picard_zero line 206
  23. theorem OAI.MorseArnold.SmoothODE.exists_smooth_local_inverse line 221
  24. theorem OAI.MorseArnold.SmoothODE.mul_mem_time line 248
  25. def OAI.MorseArnold.SmoothODE.flowDomain line 256
  26. def OAI.MorseArnold.SmoothODE.rescaledPath line 262
  27. theorem OAI.MorseArnold.SmoothODE.rescaledPath_apply line 269
  28. theorem OAI.MorseArnold.SmoothODE.continuous_rescaledPath line 273
  29. def OAI.MorseArnold.SmoothODE.rescaledPaths line 279
  30. theorem OAI.MorseArnold.SmoothODE.rescaledPaths_of_mem line 284
  31. theorem OAI.MorseArnold.SmoothODE.continuousOn_rescaledPaths line 290
  32. theorem OAI.MorseArnold.SmoothODE.rescaledPaths_initial line 297
  33. theorem OAI.MorseArnold.SmoothODE.picardMap_rescaledPaths line 306
  34. theorem OAI.MorseArnold.SmoothODE.smooth_flow_near_origin line 343
  35. theorem OAI.MorseArnold.SmoothODE.exists_local_smooth_flow line 386
  36. def OAI.MorseArnold.SmoothODE.LocalSmoothFlowExistence line 419
  37. theorem OAI.MorseArnold.SmoothODE.localSmoothFlowExistence line 429