OAI/Probability/CriticalPercolation/Growth/CosetBallIndex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.CosetGrowth.ball line 13
2. lemma OAI.CriticalPercolation.CosetGrowth.ball_zero line 16
3. lemma OAI.CriticalPercolation.CosetGrowth.ball_step line 19
4. lemma OAI.CriticalPercolation.CosetGrowth.ball_mono line 29
5. lemma OAI.CriticalPercolation.CosetGrowth.ball_one_mem line 32
6. lemma OAI.CriticalPercolation.CosetGrowth.ball_eq_univ_of_stationary line 38
7. lemma OAI.CriticalPercolation.CosetGrowth.finiteIndex_of_small_ball line 66
8. lemma OAI.CriticalPercolation.CosetGrowth.ball_subset_coset_representatives line 93
9. theorem OAI.CriticalPercolation.CosetGrowth.finiteIndex_of_few_cosets line 103