OAI/Combinatorics/Progressions/Estimates/RealProjectedCoefficientLift.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.lieTreeEval_hom line 10
  2. def OAI.Erdos3.DegreeRankLieFiltration.horizontalProjectionMap line 25
  3. def OAI.Erdos3.DegreeRankLieFiltration.horizontalProjectionImage line 31
  4. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_horizontalProjectionImage line 35
  5. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalProjectionImage_frequency line 40
  6. def OAI.Erdos3.DegreeRankLieFiltration.layerHorizontalMap line 92
  7. def OAI.Erdos3.DegreeRankLieFiltration.layerHorizontalImage line 98
  8. theorem OAI.Erdos3.DegreeRankLieFiltration.mem_layerHorizontalImage line 101
  9. theorem OAI.Erdos3.DegreeRankLieFiltration.layerHorizontalImage_frequency line 105
  10. theorem OAI.Erdos3.DegreeRankLieFiltration.projected_sunflower_bracket line 150
  11. theorem OAI.Erdos3.DegreeRankLieFiltration.projected_sunflower_representatives line 166
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.layer_sunflower_bracket line 198
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.layer_sunflower_representatives line 214
  14. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedComponent_mem_layer line 248
  15. def OAI.Erdos3.DegreeRankLieFiltration.projectedComponentSymbolMap line 254
  16. def OAI.Erdos3.DegreeRankLieFiltration.projectedHorizontalSymbolCoefficient line 259
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedHorizontalSymbolCoefficient_symbol line 264
  18. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedHorizontalSymbolCoefficient_lie line 279
  19. def OAI.Erdos3.DegreeRankLieFiltration.realProjectedHorizontalSymbolHom line 303
  20. theorem OAI.Erdos3.DegreeRankLieFiltration.realProjectedHorizontalSymbolHom_apply line 321
  21. theorem OAI.Erdos3.DegreeRankLieFiltration.real_projectedHorizontalSymbolCoefficient_component line 326
  22. def OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalMap line 351
  23. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalMap_baseChange line 357
  24. def OAI.Erdos3.DegreeRankLieFiltration.projectedLayerCoefficient line 367
  25. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedLayerCoefficient_coe line 373
  26. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedLayerCoefficient_horizontal line 377
  27. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedLayerCoefficient_tensor_coe line 384
  28. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedLayerCoefficient_tensor_horizontal line 396
  29. theorem OAI.Erdos3.DegreeRankLieFiltration.real_projectedCoefficient_mem line 415
  30. theorem OAI.Erdos3.DegreeRankLieFiltration.real_projectedCoefficient_horizontal line 424