OAI/Probability/CriticalPercolation/Modular/ClusterDiscrepancy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.clusterSize line 19
2. lemma OAI.CriticalPercolation.BondGraph.cluster_eq_of_reachable line 23
3. lemma OAI.CriticalPercolation.BondGraph.cluster_disjoint_of_not_reachable line 29
4. lemma OAI.CriticalPercolation.BondGraph.clusterSize_pos line 35
5. lemma OAI.CriticalPercolation.BondGraph.clusterSize_eq_of_reachable line 39
6. def OAI.CriticalPercolation.BondGraph.rootMass line 44
7. lemma OAI.CriticalPercolation.BondGraph.sum_rootMass_cluster line 47
8. lemma OAI.CriticalPercolation.BondGraph.incident_cluster_iff line 67
9. lemma OAI.CriticalPercolation.BondGraph.sum_incident_rootMass line 80
10. lemma OAI.CriticalPercolation.BondGraph.cluster_insert_endpoint line 103
11. lemma OAI.CriticalPercolation.BondGraph.clusterSize_insert_of_disconnected line 117
12. lemma OAI.CriticalPercolation.BondGraph.clusterSize_insert_of_connected line 124