OAI/Combinatorics/Progressions/Estimates/RealifiedTripleLayers.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.weightedSubalgebra line 13
  2. def OAI.Erdos3.MultidegreeLieFiltration.weightedFiltration line 16
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_weightedFiltration_layer line 39
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedFiltration_layer_map line 45
  5. theorem OAI.Erdos3.multidegreeWeight_le_sum line 66
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_le_ordinary line 77
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.coordinateIdeal_abelian line 86
  8. def OAI.Erdos3.MultidegreeLieFiltration.coordinateActiveLayer line 110
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.coordinateActiveLayer_antitone line 113
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.weighted_lie_active line 116
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.active_lie_weighted line 122
  12. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer line 128
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_additiveTripleLayer line 134
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer_antitone line 140
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer_lie_mem line 145
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer_coordinates line 168
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer_terminal line 179
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleLayer_top_relation line 187
  19. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleSubalgebra line 206
  20. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleFiltration line 212
  21. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleFirst line 231
  22. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleSecond line 236
  23. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleThird line 242
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleProjections_mem line 248
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleTop_relation line 257
  26. def OAI.Erdos3.tripleToPi line 275
  27. theorem OAI.Erdos3.tripleToPi_zero line 280
  28. theorem OAI.Erdos3.tripleToPi_one line 282
  29. theorem OAI.Erdos3.tripleToPi_two line 284
  30. theorem OAI.Erdos3.tripleToPi_injective line 286
  31. def OAI.Erdos3.MultidegreeLieFiltration.additiveTripleToPi line 295
  32. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleToPi_injective line 300
  33. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTripleToPi_mem line 305
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.weightedLayer_realification line 333
  35. def OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedEquiv line 340
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedEquiv_coe line 345
  37. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedEquiv_mem_layer line 349
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedEquiv_symm_mem_layer line 366
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.coordinateActiveLayer_realification line 385
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.realTripleEquiv_mem_layer line 391
  41. def OAI.Erdos3.MultidegreeLieFiltration.realifiedTripleLayerEquiv line 409
  42. def OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleEquiv line 420
  43. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleEquiv_coe line 427
  44. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleEquiv_mem_layer line 434
  45. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleEquiv_symm_mem_layer line 450