OAI/Probability/CriticalPercolation/Modular/ClusterTransportFinite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteClusters.transport_row_zero line 14
2. lemma OAI.CriticalPercolation.FiniteClusters.transport_column_zero line 24
3. lemma OAI.CriticalPercolation.FiniteClusters.mass_le_one line 39
4. lemma OAI.CriticalPercolation.FiniteClusters.weight_le_one line 46
5. lemma OAI.CriticalPercolation.FiniteClusters.transport_bound line 52
6. lemma OAI.CriticalPercolation.FiniteClusters.transport_aut line 61
7. lemma OAI.CriticalPercolation.FiniteClusters.measurable_weight line 66
8. lemma OAI.CriticalPercolation.FiniteClusters.measurable_transport line 69
9. lemma OAI.CriticalPercolation.FiniteClusters.integrable_transport line 74
10. def OAI.CriticalPercolation.FiniteClusters.expectedTransport line 79
11. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_aut line 82
12. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_row_zero line 92
13. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_column_zero line 98
14. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_row_finite line 105
15. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_column_finite line 113
16. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_sum_out line 121
17. lemma OAI.CriticalPercolation.FiniteClusters.expectedTransport_sum_in line 135