OAI/Probability/CriticalPercolation/Growth/CosetSparseGrowth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.RelativeGrowth.ball line 14
2. def OAI.CriticalPercolation.RelativeGrowth.HasDegree line 17
3. lemma OAI.CriticalPercolation.RelativeGrowth.ball_mono line 20
4. lemma OAI.CriticalPercolation.RelativeGrowth.not_quadratic_exponential_lower line 23
5. lemma OAI.CriticalPercolation.RelativeGrowth.binaryProducts_coset_inj line 52
6. lemma OAI.CriticalPercolation.RelativeGrowth.binaryProducts_subset_pow line 83
7. lemma OAI.CriticalPercolation.RelativeGrowth.no_linear_strict_chain line 102