OAI/Combinatorics/Progressions/Estimates/CommonFreeSunflower.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_horizontal_frequency line 24
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_sunflower_bracket line 44
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_sunflower_representatives line 60
4. def OAI.Erdos3.NativeRankRelation.CommonData.commonCoefficientSpace line 97
5. def OAI.Erdos3.NativeRankRelation.CommonData.dependentCoefficientSpace line 100
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonCoefficientSpace_le line 103
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentCoefficientSpace_le_common line 107
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.native_coefficient_mem_common line 111
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.native_coefficient_mem_dependent line 129
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficient_sunflower line 147
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_coefficient_sunflower line 162
12. structure OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases line 200
13. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.mono line 210
14. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientAlphabet line 217
15. instance OAI.Erdos3.NativeRankRelation.CommonData.coefficientAlphabetFintype line 221
16. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientDegree line 225
17. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientWeight line 228
18. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientWeight_pos line 230
19. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientAlphabet_card line 235
20. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator line 250
21. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator_mem_common line 254
22. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator_mem_layer line 261
23. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator_height line 267
24. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator_common_span line 274
25. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.generator_dependent_span line 279
26. def OAI.Erdos3.coefficientSpaceInputBudget line 292
27. def OAI.Erdos3.coefficientSpaceBasisBudget line 295
28. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficient_space_bases line 314
29. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientFourSpace line 429
30. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFourSpace_le line 433
31. theorem OAI.Erdos3.NativeRankRelation.CommonData.mem_coefficientFourSpace line 438
32. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficient_four_frequency line 449
33. abbrev OAI.Erdos3.NativeRankRelation.CommonData.CoefficientFreeLieAlgebra line 496
34. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeFiltration line 499
35. def OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeGenerator line 503
36. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeGenerator_mem_layer line 506
37. def OAI.Erdos3.NativeRankRelation.CommonData.commonFreeSpan line 510
38. def OAI.Erdos3.NativeRankRelation.CommonData.dependentFreeSpan line 513
39. theorem OAI.Erdos3.NativeRankRelation.CommonData.commonFreeSpan_le_layer line 516
40. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentFreeSpan_le_layer line 522
41. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation line 530
42. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_generator line 534
43. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.commonFreeLift line 538
44. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.dependentFreeLift line 542
45. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.commonFreeLift_range line 546
46. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.dependentFreeLift_range line 550
47. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_commonFreeLift line 554
48. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_dependentFreeLift line 566
49. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realCommonFreeLift line 600
50. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realDependentFreeLift line 606
51. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realCommonFreeLift_baseChange line 612
52. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realDependentFreeLift_baseChange line 619
53. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realCommonFreeLift_mem line 626
54. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realDependentFreeLift_mem line 638
55. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realEvaluation_commonFreeLift line 650
56. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realEvaluation_dependentFreeLift line 663
57. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_commonFreeSpan line 698
58. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeEvaluation_dependentFreeSpan line 713
59. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realEvaluation_commonFreeSpan line 728
60. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.realEvaluation_dependentFreeSpan line 735
61. def OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.freeFrequency line 742
62. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.free_sunflower line 745
63. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_free_sunflower line 761