OAI/Probability/CriticalPercolation/Modular/ClusterTransportSums.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteClusters.weight line 14
2. def OAI.CriticalPercolation.FiniteClusters.transport line 17
3. def OAI.CriticalPercolation.FiniteClusters.clusterWeight line 20
4. def OAI.CriticalPercolation.FiniteClusters.truncatedEdgeMass line 23
5. lemma OAI.CriticalPercolation.FiniteClusters.weight_reachable line 28
6. lemma OAI.CriticalPercolation.FiniteClusters.weight_nonneg line 32
7. lemma OAI.CriticalPercolation.FiniteClusters.clusterWeight_nonneg line 38
8. lemma OAI.CriticalPercolation.FiniteClusters.clusterWeight_le line 44
9. lemma OAI.CriticalPercolation.FiniteClusters.weighted_cluster_summable line 51
10. lemma OAI.CriticalPercolation.FiniteClusters.tsum_weighted_cluster line 68
11. lemma OAI.CriticalPercolation.FiniteClusters.transport_sum_out line 94
12. lemma OAI.CriticalPercolation.FiniteClusters.transport_sum_in line 105
13. lemma OAI.CriticalPercolation.FiniteClusters.truncatedEdgeMass_nonneg line 142
14. lemma OAI.CriticalPercolation.FiniteClusters.truncatedEdgeMass_le line 149
15. lemma OAI.CriticalPercolation.FiniteClusters.transport_sum_in_bound line 156