OAI/Combinatorics/Progressions/Estimates/LieTreeMultidegree.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.lieTreeWeight line 14
  2. theorem OAI.Erdos3.lieTree_length_le_weight line 18
  3. def OAI.Erdos3.weightedLieTreeGenerators line 24
  4. def OAI.Erdos3.weightedLieTreeSpan line 27
  5. theorem OAI.Erdos3.weightedLieTreeSpan_antitone line 30
  6. theorem OAI.Erdos3.weightedLieTreeSpan_lie_mem line 37
  7. theorem OAI.Erdos3.span_weighted_leaves_le line 52
  8. theorem OAI.Erdos3.FilteredLieTree.eval_mem_weighted_span line 58
  9. theorem OAI.Erdos3.NilpotentLieFiltration.lieTreeEval_mem_rankLayer line 70
  10. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_eq_weighted_tree_span line 77
  11. def OAI.Erdos3.finiteLieTrees line 107
  12. theorem OAI.Erdos3.mem_finiteLieTrees_of_length_le line 114
  13. theorem OAI.Erdos3.finiteLieTrees_card_le line 136
  14. def OAI.Erdos3.finiteWeightedLieValues line 169
  15. theorem OAI.Erdos3.weightedLieTreeSpan_eq_finite_span line 174
  16. theorem OAI.Erdos3.finiteWeightedLieValues_card_le line 193
  17. theorem OAI.Erdos3.lieTreeEval_relabel line 208
  18. theorem OAI.Erdos3.lieTreeWeight_relabel line 216
  19. theorem OAI.Erdos3.lieTreeLength_relabel line 224
  20. theorem OAI.Erdos3.lieTreeSupport_relabel line 232
  21. abbrev OAI.Erdos3.LieTreeOccurrences line 241
  22. instance OAI.Erdos3.lieTreeOccurrencesFintype line 245
  23. def OAI.Erdos3.lieTreeOccurrenceLabel line 253
  24. def OAI.Erdos3.lieTreeOccurrenceTree line 257
  25. theorem OAI.Erdos3.lieTreeOccurrenceTree_eval line 262
  26. theorem OAI.Erdos3.lieTreeOccurrenceTree_weight line 272
  27. theorem OAI.Erdos3.lieTreeOccurrenceTree_length line 282
  28. theorem OAI.Erdos3.lieTreeOccurrenceTree_support line 292
  29. def OAI.Erdos3.bracketMultilinear line 321
  30. theorem OAI.Erdos3.bracketMultilinear_apply line 340
  31. def OAI.Erdos3.lieTreeOccurrenceMultilinear line 345
  32. theorem OAI.Erdos3.lieTreeOccurrenceMultilinear_apply line 350
  33. theorem OAI.Erdos3.lieTreeOccurrenceMultilinear_original line 364
  34. theorem OAI.Erdos3.exists_linear_lieTree_expansion line 368
  35. def OAI.Erdos3.lieTreeMarkedCount line 407
  36. theorem OAI.Erdos3.lieTreeMarkedCount_leaf line 410
  37. theorem OAI.Erdos3.lieTreeMarkedCount_mul line 413
  38. theorem OAI.Erdos3.lieTreeMarkedCount_le_length line 417
  39. theorem OAI.Erdos3.lieTreeWeight_eq_sum_occurrences line 423
  40. theorem OAI.Erdos3.lieTreeMarkedCount_eq_card line 434
  41. theorem OAI.Erdos3.exists_two_marked_occurrences line 441
  42. theorem OAI.Erdos3.multilinear_eq_of_one_vanish line 461
  43. theorem OAI.Erdos3.lieTree_eq_of_one_petal_vanish line 484
  44. def OAI.Erdos3.lieTreeMultidegree line 518
  45. theorem OAI.Erdos3.lieTreeMultidegree_leaf line 522
  46. theorem OAI.Erdos3.lieTreeMultidegree_mul line 525
  47. theorem OAI.Erdos3.lieTreeMultidegree_apply line 528
  48. def OAI.Erdos3.markedGeneratorGrade line 534
  49. theorem OAI.Erdos3.markedTreeGrade_weight line 537
  50. theorem OAI.Erdos3.markedTreeGrade_count line 542
  51. theorem OAI.Erdos3.markedTreeGrade_length line 547