OAI/Probability/CriticalPercolation/GraphGeometry/GraphBalls.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.vertexBall_mono line 16
2. lemma OAI.CriticalPercolation.BondGraph.mem_vertexBall_self line 21
3. lemma OAI.CriticalPercolation.BondGraph.vertexBall_step line 24
4. lemma OAI.CriticalPercolation.BondGraph.vertexBall_add line 28
5. lemma OAI.CriticalPercolation.BondGraph.vertexBall_comm line 38
6. lemma OAI.CriticalPercolation.BondGraph.Aut.fullGraph_adj line 52
7. lemma OAI.CriticalPercolation.BondGraph.Aut.vertexBall_mem line 56
8. lemma OAI.CriticalPercolation.BondGraph.Aut.vertexBall_image line 72
9. lemma OAI.CriticalPercolation.BondGraph.Aut.vertexBall_ncard line 79
10. lemma OAI.CriticalPercolation.BondGraph.Aut.incident_singleton_image line 83
11. lemma OAI.CriticalPercolation.BondGraph.uniform_incident_bound line 91
12. lemma OAI.CriticalPercolation.BondGraph.uniform_ball_bound line 101
13. lemma OAI.CriticalPercolation.BondGraph.orbit_density_radius line 110
14. lemma OAI.CriticalPercolation.BondGraph.finite_subset_vertexBall line 126