OAI/Geometry/NilpotentCharts/CentralAxes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Central tangent directions, central axes and local quotient slices.

  1. lemma OAI.RawLieIntegration.invariantField_hom line 19
  2. lemma OAI.RawLieIntegration.integralCurve_hom line 46
  3. lemma OAI.RawLieIntegration.curve_hom line 62
  4. lemma OAI.RawLieIntegration.curve_central line 76
  5. lemma OAI.RawLieIntegration.curve_nonconstant line 88
  6. theorem OAI.RawLieIntegration.exists_central_axis line 99
  7. def OAI.RawLieAdjoint.centralTangent line 121
  8. lemma OAI.RawLieAdjoint.mem_centralTangent line 125
  9. lemma OAI.RawLieAdjoint.exists_finite_inf line 130
  10. lemma OAI.RawLieAdjoint.centralTangent_finite_test line 155
  11. lemma OAI.RawLieAdjoint.centralTangent_curve line 164
  12. lemma OAI.RawLieAdjoint.centralTangent_ne_bot line 173
  13. lemma OAI.RawLieIntegration.orderedAxes_mem_center line 191
  14. lemma OAI.RawLieIntegration.orderedAxes_add_of_central line 199
  15. lemma OAI.RawLieIntegration.subspaceAxes_central line 219
  16. lemma OAI.RawLieIntegration.subspaceAxes_central_add line 223
  17. def OAI.RawLieIntegration.centralAxesHom line 231
  18. lemma OAI.RawLieIntegration.centralAxesHom_continuous line 236
  19. lemma OAI.RawLieIntegration.centralAxesHom_range_le_center line 239
  20. lemma OAI.RawLieIntegration.transverse_test_derivative line 254
  21. lemma OAI.RawLieIntegration.transverse_test_contDiffAt line 266
  22. theorem OAI.RawLieIntegration.exists_transverse_neighbourhood line 278
  23. theorem OAI.RawLieIntegration.centralAxesHom_locally_surjective line 332
  24. theorem OAI.RawLieIntegration.centralAxesHom_range_isClosed line 364
  25. theorem OAI.RawLieIntegration.exists_quotient_injective_neighbourhood line 404
  26. lemma OAI.RawLieIntegration.quotient_productSlice line 470
  27. theorem OAI.RawLieIntegration.exists_central_quotient_openChart line 481