OAI/Probability/CriticalPercolation/Modular/HeavyClusterNumber.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.modularMass_union_le line 18
2. lemma OAI.CriticalPercolation.BondGraph.modularMass_finite_biUnion_lt_top line 26
3. lemma OAI.CriticalPercolation.BondGraph.heavy_cluster_union_has_old line 36
4. def OAI.CriticalPercolation.BondGraph.atMostOneHeavy line 69
5. def OAI.CriticalPercolation.BondGraph.heavyClusterCover line 73
6. def OAI.CriticalPercolation.BondGraph.infinitelyManyHeavyClusters line 76
7. lemma OAI.CriticalPercolation.BondGraph.measurableSet_atMostOneHeavy line 80
8. lemma OAI.CriticalPercolation.BondGraph.measurable_heavyClusterCover line 87
9. lemma OAI.CriticalPercolation.BondGraph.infinitelyManyHeavyClusters_iff_no_finite_cover line 92
10. lemma OAI.CriticalPercolation.BondGraph.measurable_infinitelyManyHeavyClusters line 98
11. lemma OAI.CriticalPercolation.BondGraph.Aut.atMostOneHeavy_image_iff line 103
12. lemma OAI.CriticalPercolation.BondGraph.atMostOneHeavy_union_of_cover line 118
13. lemma OAI.CriticalPercolation.BondGraph.no_finite_heavyClusterCover_ae_of_unique_null line 129
14. theorem OAI.CriticalPercolation.BondGraph.unique_heavy_or_infinitely_many_ae line 148