OAI/Geometry/NilpotentCharts/AdjointPolynomials.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Polynomial one-parameter adjoint actions and triangular infinitesimal matrices.

  1. theorem OAI.RawNilpotentPolynomial.oneParameter_eq_exp line 20
  2. lemma OAI.RawNilpotentPolynomial.exp_nilpotent line 47
  3. theorem OAI.RawNilpotentPolynomial.oneParameter_polynomial line 60
  4. lemma OAI.RawNilpotentPolynomial.generator_nilpotent line 69
  5. theorem OAI.RawNilpotentPolynomial.unipotent_oneParameter_polynomial line 75
  6. lemma OAI.RawLieAdjoint.adjoint_one line 90
  7. lemma OAI.RawLieAdjoint.adjoint_mul line 96
  8. lemma OAI.RawLieAdjoint.adjoint_sub_one_nilpotent line 107
  9. lemma OAI.RawLieAdjoint.adjoint_curve_contDiff line 119
  10. theorem OAI.RawLieAdjoint.adjoint_curve_polynomial line 131
  11. lemma OAI.RawLieAdjoint.adjoint_contMDiff line 157
  12. def OAI.RawLieAdjoint.infinitesimal line 163
  13. lemma OAI.RawLieAdjoint.infinitesimal_hasDerivAt line 166
  14. lemma OAI.RawLieAdjoint.adjoint_curve_self line 188
  15. lemma OAI.RawLieAdjoint.infinitesimal_self line 200
  16. lemma OAI.RawLieAdjoint.infinitesimal_antisymm line 209
  17. lemma OAI.RawLieAdjoint.infinitesimal_triangular line 223
  18. lemma OAI.RawLieAdjoint.infinitesimal_axis_row line 241
  19. lemma OAI.RawLieAdjoint.infinitesimal_nilpotent line 247
  20. lemma OAI.RawLieAdjoint.adjoint_curve_eq_sum line 255
  21. lemma OAI.RawLieAdjoint.adjoint_axis_row line 267
  22. lemma OAI.RawLieAdjoint.polynomial_adjoint_curve line 298
  23. lemma OAI.RawLieAdjoint.polynomial_adjoint_orderedAxes_inv line 313
  24. lemma OAI.RawLieAdjoint.polynomial_adjoint_axisTail_inv line 332
  25. lemma OAI.RawLieAdjoint.polynomial_normalizedAxes_column line 345