OAI/Probability/CriticalPercolation/Modular/PeakClusters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.clusterPeak line 14
2. def OAI.CriticalPercolation.BondGraph.clusterPeaks line 17
3. def OAI.CriticalPercolation.BondGraph.peakBound line 20
4. lemma OAI.CriticalPercolation.BondGraph.clusterPeaks_eq_of_reachable line 23
5. lemma OAI.CriticalPercolation.BondGraph.peakBound_iff_of_reachable line 28
6. lemma OAI.CriticalPercolation.BondGraph.Aut.clusterPeak_iff line 33
7. lemma OAI.CriticalPercolation.BondGraph.Aut.clusterPeaks_image line 46
8. lemma OAI.CriticalPercolation.BondGraph.Aut.peakBound_iff line 54
9. lemma OAI.CriticalPercolation.BondGraph.measurable_clusterPeak line 68
10. lemma OAI.CriticalPercolation.BondGraph.measurable_mem_clusterPeaks line 72
11. lemma OAI.CriticalPercolation.BondGraph.measurable_peakBound line 76