OAI/Probability/CriticalPercolation/Harmonic/WeakGromovHarmonic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.SparseGrowth.infinite_finiteIndex_subgroup line 16
2. lemma OAI.CriticalPercolation.SparseGrowth.indicability_of_finiteIndex line 24
3. lemma OAI.CriticalPercolation.SparseGrowth.indicability_of_surjective line 36
4. lemma OAI.CriticalPercolation.SparseGrowth.HasPolynomialDegree.linear_virtually_indicable line 53
5. theorem OAI.CriticalPercolation.SparseGrowth.sparse_polynomial_virtuallyNilpotent line 76