OAI/Probability/CriticalPercolation/Gluing/StripMoves.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.cluster_induced_subset line 21
2. lemma OAI.CriticalPercolation.BondGraph.infinite_strip_unbounded line 26
3. lemma OAI.CriticalPercolation.BondGraph.strip_cluster_gives_exit line 43
4. def OAI.CriticalPercolation.BondGraph.stripPercolates line 57
5. def OAI.CriticalPercolation.BondGraph.someStripPercolates line 60
6. lemma OAI.CriticalPercolation.BondGraph.stripPercolates_measurable line 63
7. lemma OAI.CriticalPercolation.BondGraph.someStripPercolates_measurable line 67
8. lemma OAI.CriticalPercolation.BondGraph.stripPercolates_diff_iff line 71
9. lemma OAI.CriticalPercolation.BondGraph.someStripPercolates_zero_one line 79
10. def OAI.CriticalPercolation.BondGraph.seedStripInfinite line 93
11. lemma OAI.CriticalPercolation.BondGraph.seedStripInfinite_measurable line 96
12. lemma OAI.CriticalPercolation.BondGraph.seedStripInfinite_mono line 109
13. lemma OAI.CriticalPercolation.BondGraph.seedStripInfinite_exhaustion line 115
14. theorem OAI.CriticalPercolation.BondGraph.exists_seed_strip_probability line 129