OAI/Geometry/NilpotentCharts/AxesDerivatives.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Smooth inverse coordinates and triangular differential equations for multiplication.

  1. lemma OAI.RawLieIntegration.adjoint_orderedAxes_inv_prefix line 19
  2. lemma OAI.RawLieIntegration.axisTail_eq_orderedAxes_mask line 59
  3. lemma OAI.RawLieIntegration.adjoint_axisTail_inv_prefix line 74
  4. def OAI.RawLieIntegration.normalizedAxes line 100
  5. lemma OAI.RawLieIntegration.normalizedAxes_contMDiff line 103
  6. lemma OAI.RawLieIntegration.normalizedAxes_self line 107
  7. lemma OAI.RawLieIntegration.normalizedAxes_shift line 110
  8. lemma OAI.RawLieIntegration.normalizedAxes_derivative_column line 115
  9. lemma OAI.RawLieIntegration.normalizedAxes_derivative_injective line 152
  10. lemma OAI.RawLieIntegration.orderedAxes_derivative_equiv line 173
  11. lemma OAI.RawLieIntegration.orderedAxes_inverse_contMDiff line 201
  12. def OAI.RawLieIntegration.coordinateProduct line 216
  13. lemma OAI.RawLieIntegration.orderedAxes_coordinateProduct line 219
  14. lemma OAI.RawLieIntegration.coordinateProduct_contDiff line 226
  15. lemma OAI.RawLieIntegration.normalizedAxes_coordinateProduct line 233
  16. lemma OAI.RawLieIntegration.coordinateProduct_normalized_derivative line 240
  17. def OAI.RawLieIntegration.coordinateMC line 256
  18. lemma OAI.RawLieIntegration.coordinateMC_column line 261
  19. lemma OAI.RawLieIntegration.coordinateMC_triangular line 267
  20. lemma OAI.RawLieIntegration.coordinateMC_product_derivative line 278
  21. lemma OAI.RawLieIntegration.coordinateMC_polynomials line 295
  22. def OAI.RawLieIntegration.coordinateLine line 313
  23. lemma OAI.RawLieIntegration.coordinateLine_zero line 316
  24. lemma OAI.RawLieIntegration.coordinateLine_hasDerivAt line 325
  25. lemma OAI.RawLieIntegration.coordinateLine_ode line 334