OAI/Combinatorics/Progressions/Estimates/MultidegreeIntegralModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralModel line 21
2. def OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralStructure line 33
3. theorem OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralModel_basis line 39
4. theorem OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralStructure_filtration line 41
5. theorem OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralModel_coordinates line 44
6. theorem OAI.Erdos3.MultidegreeLieFiltration.boundedIntegralStructure_complexity line 49
7. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_bounded_integral_model line 63