OAI/Combinatorics/Progressions/Polynomial/TotalDegreeSplitDownsets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.totalDegree_zero_layer line 16
  2. def OAI.Erdos3.NilpotentLieFiltration.totalDegreeMultifiltration line 21
  3. theorem OAI.Erdos3.NilpotentLieFiltration.totalDegreeMultifiltration_layer line 55
  4. theorem OAI.Erdos3.NilpotentLieFiltration.totalDegreeMultifiltration_real_layer line 58
  5. theorem OAI.Erdos3.NilpotentLieFiltration.totalDegree_adapted line 77
  6. def OAI.Erdos3.NilpotentLieFiltration.totalDegreeOrbit line 84
  7. theorem OAI.Erdos3.NilpotentLieFiltration.totalDegreeOrbit_eval line 88
  8. theorem OAI.Erdos3.NilpotentLieFiltration.real_totalDegree_adapted line 92
  9. def OAI.Erdos3.NilpotentLieFiltration.realTotalDegreeOrbit line 99
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realTotalDegreeOrbit_eval line 104
  11. def OAI.Erdos3.totalDegreeSplitBound line 119
  12. def OAI.Erdos3.totalDegreeSplitDownset line 122
  13. theorem OAI.Erdos3.totalDegreeSplitBound_le line 125
  14. theorem OAI.Erdos3.totalDegreeSplitDownset_lower line 130
  15. theorem OAI.Erdos3.mem_totalDegreeSplitDownset_false line 134
  16. theorem OAI.Erdos3.mem_totalDegreeSplitDownset_true line 138
  17. theorem OAI.Erdos3.totalDegreeSplitDownset_covers line 142
  18. theorem OAI.Erdos3.totalDegreeSplitDownset_terminal line 150