OAI/Probability/CriticalPercolation/Modular/OrbitalMassTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.swapPairOrbitFn line 15
2. def OAI.CriticalPercolation.BondGraph.swapPairOrbit line 21
3. lemma OAI.CriticalPercolation.BondGraph.swapPairOrbit_mk line 27
4. def OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.weightedRow line 33
5. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.weightedRow_finite line 36
6. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.fiber_sum_root line 46
7. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.fiber_sum line 68
8. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.tsum_weightedRow line 83
9. lemma OAI.CriticalPercolation.BondGraph.OrbitRepresentatives.massTransport line 91