OAI/Probability/CriticalPercolation/Growth/CosetGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CriticalPercolation.RelativeGrowth.Presentation line 16
2. abbrev OAI.CriticalPercolation.RelativeGrowth.Presentation.X line 26
3. abbrev OAI.CriticalPercolation.RelativeGrowth.Presentation.projection line 27
4. abbrev OAI.CriticalPercolation.RelativeGrowth.Presentation.root line 28
5. def OAI.CriticalPercolation.RelativeGrowth.Presentation.graph line 30
6. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.adj_mk_iff line 39
7. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.smul_adj_iff line 48
8. def OAI.CriticalPercolation.RelativeGrowth.Presentation.actionAut line 60
9. def OAI.CriticalPercolation.RelativeGrowth.Presentation.actionHom line 63
10. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.actionAut_mk line 67
11. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.reachable_mk line 69
12. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.connected line 87
13. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.neighbors_subset line 94
14. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.locallyFinite line 99
15. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.transitive line 103
16. def OAI.CriticalPercolation.RelativeGrowth.Presentation.geometry line 107
17. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.walk_endpoint line 110
18. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.reachBall_subset line 122
19. lemma OAI.CriticalPercolation.RelativeGrowth.Presentation.geometry_hasDegree line 126