OAI/Probability/CriticalPercolation/Growth/PolynomialGrowthDescent.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.SparseGrowth.HasDegree line 13
2. lemma OAI.CriticalPercolation.SparseGrowth.cyclic_inter_lower_bound line 16
3. lemma OAI.CriticalPercolation.SparseGrowth.quotient_linear_packing line 34
4. theorem OAI.CriticalPercolation.SparseGrowth.quotient_degree_descent line 47
5. theorem OAI.CriticalPercolation.SparseGrowth.finite_of_degree_zero line 79
6. theorem OAI.CriticalPercolation.SparseGrowth.virtuallyNilpotent_of_central_kernel line 94
7. theorem OAI.CriticalPercolation.SparseGrowth.virtuallyNilpotent_of_finiteIndex line 119
8. lemma OAI.CriticalPercolation.SparseGrowth.exists_mem_pow line 129
9. lemma OAI.CriticalPercolation.SparseGrowth.finite_subset_word_ball line 146
10. theorem OAI.CriticalPercolation.SparseGrowth.degree_of_injective line 155
11. def OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree line 185
12. lemma OAI.CriticalPercolation.SparseGrowth.hasPolynomialDegree_iff line 189
13. lemma OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.fg line 211
14. lemma OAI.CriticalPercolation.SparseGrowth.exists_symmetric_generators line 215
15. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.of_injective line 229
16. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.finiteIndex_subgroup line 236
17. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.finite line 241
18. theorem OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.quotient_descent line 245
19. lemma OAI.CriticalPercolation.SparseGrowth.virtuallyNilpotent_of_finite line 259
20. def OAI.CriticalPercolation.SparseGrowth.BadDegree line 264
21. theorem OAI.CriticalPercolation.SparseGrowth.minimal_counterexample_center_torsion line 268