OAI/Probability/CriticalPercolation/Modular/ModularClusterCount.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.reciprocalClusterMass line 16
2. def OAI.CriticalPercolation.BondGraph.finiteMassIndicator line 19
3. lemma OAI.CriticalPercolation.BondGraph.reciprocalClusterMass_le_one line 22
4. lemma OAI.CriticalPercolation.BondGraph.measurable_reciprocalClusterMass line 25
5. lemma OAI.CriticalPercolation.BondGraph.measurable_finiteMassIndicator line 29
6. lemma OAI.CriticalPercolation.BondGraph.Aut.reciprocalClusterMass line 33
7. lemma OAI.CriticalPercolation.BondGraph.finiteMassIndicator_eq_of_reachable line 38
8. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_mul_reverse line 44
9. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_inv line 48
10. lemma OAI.CriticalPercolation.BondGraph.reciprocalClusterMass_change_base line 54
11. lemma OAI.CriticalPercolation.BondGraph.sum_reciprocalClusterMass line 62
12. def OAI.CriticalPercolation.BondGraph.incidentClusterCount line 81
13. lemma OAI.CriticalPercolation.BondGraph.measurable_incidentClusterCount line 84
14. lemma OAI.CriticalPercolation.BondGraph.incident_cluster_iff_ends line 91
15. lemma OAI.CriticalPercolation.BondGraph.incidentClusterCount_of_ends line 103
16. lemma OAI.CriticalPercolation.BondGraph.incidentClusterCount_le_two line 122