OAI/Probability/CriticalPercolation/Growth/CosetBounded.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.RelativeGrowth.Bounded line 15
2. lemma OAI.CriticalPercolation.RelativeGrowth.bounded_singleton line 16
3. lemma OAI.CriticalPercolation.RelativeGrowth.bounded_finite line 31
4. lemma OAI.CriticalPercolation.RelativeGrowth.Bounded.mono line 44
5. lemma OAI.CriticalPercolation.RelativeGrowth.Bounded.mul line 46
6. lemma OAI.CriticalPercolation.RelativeGrowth.Bounded.inv line 49
7. lemma OAI.CriticalPercolation.RelativeGrowth.Bounded.union line 54
8. lemma OAI.CriticalPercolation.RelativeGrowth.finite_coset_image_iff_cover line 60
9. lemma OAI.CriticalPercolation.RelativeGrowth.bounded_of_finite_coset_image line 81
10. lemma OAI.CriticalPercolation.RelativeGrowth.finite_coset_image_of_bounded line 86
11. lemma OAI.CriticalPercolation.RelativeGrowth.HasDegree.bounded_generators line 92
12. lemma OAI.CriticalPercolation.RelativeGrowth.HasDegree.zero_finiteIndex line 119