OAI/Geometry/NilpotentCharts/Flows.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Invariant vector fields, one-parameter flows and ordered axes.

  1. lemma OAI.RawLieIntegration.invariant_derivative line 18
  2. lemma OAI.RawLieIntegration.integralCurveOn_leftMul line 41
  3. lemma OAI.RawLieIntegration.integralCurve_leftMul line 58
  4. lemma OAI.RawLieIntegration.invariantField_contMDiff_one line 64
  5. lemma OAI.RawLieIntegration.exists_global_integralCurve line 73
  6. theorem OAI.RawLieIntegration.exists_oneParameterSubgroup line 86
  7. def OAI.RawLieIntegration.curve line 101
  8. lemma OAI.RawLieIntegration.curve_continuous line 104
  9. lemma OAI.RawLieIntegration.curve_zero line 107
  10. lemma OAI.RawLieIntegration.curve_add line 110
  11. lemma OAI.RawLieIntegration.curve_integral line 114
  12. lemma OAI.RawLieIntegration.curve_unique line 118
  13. lemma OAI.RawLieIntegration.curve_smul line 125
  14. def OAI.RawLieIntegration.exp line 136
  15. lemma OAI.RawLieIntegration.exp_smul line 138
  16. lemma OAI.RawLieIntegration.exp_zero line 141
  17. lemma OAI.RawLieIntegration.exp_same_line_add line 144
  18. lemma OAI.RawLieIntegration.curve_neg line 148
  19. lemma OAI.RawLieIntegration.exp_neg line 152
  20. def OAI.RawLieIntegration.oneParameter line 158
  21. lemma OAI.RawLieIntegration.oneParameter_continuous line 163
  22. lemma OAI.RawLieIntegration.invariantField_one line 167
  23. lemma OAI.RawLieIntegration.curve_derivative_zero line 178
  24. lemma OAI.RawLieIntegration.curve_injective line 187
  25. lemma OAI.RawLieIntegration.invariantField_contMDiff line 200
  26. lemma OAI.RawLieIntegration.curve_contMDiff_nat line 228
  27. lemma OAI.RawLieIntegration.curve_contMDiff line 255
  28. lemma OAI.RawLieIntegration.curve_contMDiff_one line 259
  29. def OAI.RawLieIntegration.orderedAxes line 264
  30. lemma OAI.RawLieIntegration.orderedAxes_zero line 267
  31. lemma OAI.RawLieIntegration.orderedAxes_single line 271
  32. lemma OAI.RawLieIntegration.orderedAxes_contMDiff_one line 279
  33. lemma OAI.RawLieIntegration.orderedAxes_derivative_single line 298
  34. lemma OAI.RawLieIntegration.orderedAxes_derivative_basis line 323
  35. lemma OAI.RawLieIntegration.orderedAxes_chart_hasFDerivAt line 342
  36. lemma OAI.RawLieIntegration.orderedAxes_chart_contDiffAt line 376
  37. theorem OAI.RawLieIntegration.exists_orderedAxes_localChart line 389
  38. def OAI.RawLieIntegration.axesLinear line 418
  39. lemma OAI.RawLieIntegration.orderedAxes_derivative line 421
  40. def OAI.RawLieIntegration.subspaceAxes line 438
  41. lemma OAI.RawLieIntegration.subspaceAxes_zero line 441
  42. lemma OAI.RawLieIntegration.subspaceAxes_contMDiff_one line 445
  43. lemma OAI.RawLieIntegration.subspaceAxes_derivative line 449
  44. lemma OAI.RawLieIntegration.chart_comp_hasFDerivAt_one line 481
  45. lemma OAI.RawLieIntegration.exists_localChart_of_derivative line 506
  46. lemma OAI.RawLieIntegration.orderedAxes_contMDiff line 541
  47. lemma OAI.RawLieIntegration.subspaceAxes_contMDiff line 560
  48. def OAI.RawLieIntegration.vectorDerivative line 565
  49. lemma OAI.RawLieIntegration.product_derivative_zero line 569
  50. def OAI.RawLieIntegration.productSlice line 588
  51. lemma OAI.RawLieIntegration.productSlice_zero line 591
  52. lemma OAI.RawLieIntegration.productSlice_contMDiff line 594
  53. lemma OAI.RawLieIntegration.productSlice_derivative line 599
  54. theorem OAI.RawLieIntegration.exists_productSlice_localChart line 634
  55. lemma OAI.RawLieIntegration.invariantField_map line 654
  56. lemma OAI.RawLieIntegration.integralCurve_map line 682
  57. lemma OAI.RawLieIntegration.curve_map line 698
  58. lemma OAI.RawLieIntegration.orderedAxes_map line 703
  59. lemma OAI.RawLieIntegration.orderedAxes_succ line 720
  60. def OAI.RawLieIntegration.axisTail line 724
  61. lemma OAI.RawLieIntegration.orderedAxes_shift line 730