OAI/Combinatorics/Progressions/Linear/BoundedRankIntegralModel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.DegreeRankLieFiltration.boundedRankIntegralModel line 21
2. def OAI.Erdos3.DegreeRankLieFiltration.boundedRankIntegralStructure line 33
3. theorem OAI.Erdos3.DegreeRankLieFiltration.boundedRankIntegralModel_coordinates line 39
4. theorem OAI.Erdos3.DegreeRankLieFiltration.boundedRankIntegralStructure_complexity line 44
5. theorem OAI.Erdos3.DegreeRankLieFiltration.exists_bounded_rank_integral_model line 56
6. theorem OAI.Erdos3.DegreeRankLieFiltration.exists_bounded_rank_integral_model_with_frequency line 76