OAI/Combinatorics/Progressions/Estimates/DynkinTrees.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.WordPolynomial line 11
  2. def OAI.Erdos3.rightBracket line 15
  3. theorem OAI.Erdos3.rightBracket_apply line 20
  4. def OAI.Erdos3.rightBracketList line 22
  5. theorem OAI.Erdos3.rightBracketList_nil line 26
  6. theorem OAI.Erdos3.rightBracketList_cons line 27
  7. theorem OAI.Erdos3.rightBracketList_append line 30
  8. def OAI.Erdos3.rightBracketWord line 36
  9. theorem OAI.Erdos3.rightBracketWord_mul line 39
  10. def OAI.Erdos3.dynkinWord line 44
  11. theorem OAI.Erdos3.dynkinWord_mul line 47
  12. def OAI.Erdos3.wordLinearMap line 52
  13. theorem OAI.Erdos3.wordLinearMap_single line 56
  14. def OAI.Erdos3.dynkinMap line 61
  15. def OAI.Erdos3.rightAction line 64
  16. theorem OAI.Erdos3.dynkinMap_single line 67
  17. theorem OAI.Erdos3.rightAction_single line 70
  18. theorem OAI.Erdos3.rightAction_mul line 74
  19. theorem OAI.Erdos3.dynkinMap_mul line 87
  20. def OAI.Erdos3.lieTreeEval line 110
  21. def OAI.Erdos3.commutatorTree line 114
  22. theorem OAI.Erdos3.rightBracket_lie line 118
  23. theorem OAI.Erdos3.rightAction_commutatorTree line 124
  24. theorem OAI.Erdos3.dynkinMap_commutatorTree line 132