OAI/Probability/BenjaminiSchramm/OrbitTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.orbitEquiv line 16
2. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.sum_roots_eq_orbitSum line 29
3. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborCount_eq_at_vertex line 36
4. def OAI.CriticalPercolation.BondGraph.orbitNeighborTransport line 67
5. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborTransport_aut line 70
6. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborTransport_row_finite line 76
7. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborTransport_col_finite line 83
8. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborTransport_row line 92
9. def OAI.CriticalPercolation.BondGraph.weightedNeighborIncoming line 112
10. lemma OAI.CriticalPercolation.BondGraph.weightedNeighborIncoming_aut line 115
11. lemma OAI.CriticalPercolation.BondGraph.orbitNeighborTransport_incoming line 125
12. theorem OAI.CriticalPercolation.BondGraph.weightedNeighborIncoming_stationary line 135
13. theorem OAI.CriticalPercolation.BondGraph.stationaryOrbitWeight_neighbor_sum line 192
14. theorem OAI.CriticalPercolation.BondGraph.stationaryOrbitHeight_harmonic line 212