OAI/Probability/CriticalPercolation/Exploration/LayerExposure.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.measurableSet_block_of_dependsOn line 15
2. def OAI.CriticalPercolation.BondGraph.entrySeeds line 30
3. lemma OAI.CriticalPercolation.BondGraph.entrySeeds_subset_cluster line 33
4. lemma OAI.CriticalPercolation.BondGraph.measurable_entrySeeds line 37
5. lemma OAI.CriticalPercolation.BondGraph.measurableSet_entrySeed line 47
6. lemma OAI.CriticalPercolation.BondGraph.entrySeed_eq_or_adj_exterior line 52
7. lemma OAI.CriticalPercolation.BondGraph.entrySeeds_weight_band line 68
8. lemma OAI.CriticalPercolation.BondGraph.entrySeeds_weight_band_start line 90
9. lemma OAI.CriticalPercolation.BondGraph.layerStopped_eq line 119
10. lemma OAI.CriticalPercolation.BondGraph.domainLayer_restrict line 132
11. lemma OAI.CriticalPercolation.BondGraph.boundedLayer_restrict line 156
12. lemma OAI.CriticalPercolation.BondGraph.measurableSet_boundedDomainFreshExit line 163
13. lemma OAI.CriticalPercolation.BondGraph.measurableSet_boundedLayer line 172
14. lemma OAI.CriticalPercolation.BondGraph.entry_good_independent line 184