OAI/Probability/CriticalPercolation/Modular/LightClusterNumber.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.lightInfiniteEvent_change_base line 18
2. lemma OAI.CriticalPercolation.BondGraph.lightInfiniteEvent_of_reachable line 25
3. lemma OAI.CriticalPercolation.BondGraph.Aut.lightInfiniteEvent_self_iff line 36
4. def OAI.CriticalPercolation.BondGraph.lightInfinitePeaks line 43
5. def OAI.CriticalPercolation.BondGraph.lightClusterCover line 46
6. def OAI.CriticalPercolation.BondGraph.infinitelyManyLightClusters line 49
7. lemma OAI.CriticalPercolation.BondGraph.measurable_lightInfinitePeaks line 53
8. lemma OAI.CriticalPercolation.BondGraph.lightInfinitePeaks_aut line 57
9. lemma OAI.CriticalPercolation.BondGraph.lightInfinitePeaks_finite_of_cover line 64
10. lemma OAI.CriticalPercolation.BondGraph.lightInfinitePeaks_nonempty line 74
11. lemma OAI.CriticalPercolation.BondGraph.infinitelyManyLightClusters_iff_no_finite_cover line 80
12. lemma OAI.CriticalPercolation.BondGraph.measurable_infinitelyManyLightClusters line 86
13. theorem OAI.CriticalPercolation.BondGraph.light_zero_or_infinitely_many_ae line 92
14. lemma OAI.CriticalPercolation.BondGraph.light_exists_invariant line 108
15. theorem OAI.CriticalPercolation.BondGraph.infinitely_many_light_ae_of_positive line 117