OAI/Probability/BenjaminiSchramm/OrbitNeighborChain.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.BondGraph.VertexOrbit line 14
2. def OAI.CriticalPercolation.BondGraph.vertexOrbit line 16
3. lemma OAI.CriticalPercolation.BondGraph.vertexOrbit_aut line 18
4. lemma OAI.CriticalPercolation.BondGraph.orbit_out_aut line 22
5. def OAI.CriticalPercolation.BondGraph.modularWalkDegree line 27
6. lemma OAI.CriticalPercolation.BondGraph.modularWalkDegree_pos line 29
7. lemma OAI.CriticalPercolation.BondGraph.modularWalkDegree_aut line 37
8. def OAI.CriticalPercolation.BondGraph.orbitNeighborCount line 47
9. def OAI.CriticalPercolation.BondGraph.orbitWalkKernel line 50
10. lemma OAI.CriticalPercolation.BondGraph.orbitWalkKernel_nonneg line 53
11. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborCount_sum line 58
12. lemma OAI.CriticalPercolation.BondGraph.orbitWalkKernel_row_sum line 66
13. lemma OAI.CriticalPercolation.BondGraph.orbitWalkKernel_pos_of_adj line 72
14. lemma OAI.CriticalPercolation.BondGraph.orbitWalkKernel_irreducible line 88
15. theorem OAI.CriticalPercolation.BondGraph.exists_positive_orbit_stationary line 100