OAI/Combinatorics/Progressions/Estimates/CommonDependentIntegralModel.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.finiteMarkedLieValues line 14
2. theorem OAI.Erdos3.finiteMarkedLieValues_mem line 20
3. theorem OAI.Erdos3.markedLieSpan_eq_finite_span line 28
4. theorem OAI.Erdos3.finiteMarkedLieValues_card_le line 48
5. theorem OAI.Erdos3.finiteMarkedLieValues_coordinate_height line 54
6. theorem OAI.Erdos3.exists_markedLieSpan_bounded_basis line 64
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentWordLayer_inf line 102
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.top_inter_dependentWordIdeal line 108
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.top_inter_dependentWordIdeal_le_ker line 116
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_dependent_word_quotient_frequency line 122
11. theorem OAI.Erdos3.lieQuotient_mapIdeal_abelian line 138
12. abbrev OAI.Erdos3.NativeRankRelation.CommonData.DependentQuotient line 164
13. def OAI.Erdos3.NativeRankRelation.CommonData.dependentQuotientMap line 166
14. def OAI.Erdos3.NativeRankRelation.CommonData.dependentQuotientFiltration line 169
15. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentQuotientMap_mem_layer line 175
16. def OAI.Erdos3.NativeRankRelation.CommonData.dependentQuotientLinearIdeal line 179
17. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentQuotientLinearIdeal_abelian line 182
18. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_dependentQuotient_top_frequency line 189
19. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_uniform_dependentQuotient_comparison line 212
20. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_dependentQuotient_integral_model line 289