OAI/Probability/CriticalPercolation/GraphGeometry/InducedCritical.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.induce_locallyFinite line 17
2. lemma OAI.CriticalPercolation.BondGraph.induce_fullGraph_adj line 24
3. lemma OAI.CriticalPercolation.BondGraph.induce_vertexBall_subset line 29
4. lemma OAI.CriticalPercolation.BondGraph.induce_subexponential line 40
5. lemma OAI.CriticalPercolation.BondGraph.induce_percolates_subset line 53
6. lemma OAI.CriticalPercolation.BondGraph.law_induce line 62
7. lemma OAI.CriticalPercolation.BondGraph.law_induce_percolates_le line 68
8. lemma OAI.CriticalPercolation.BondGraph.criticalProbability_le_induce line 75
9. lemma OAI.CriticalPercolation.BondGraph.induce_criticalProbability_eq_of_pos line 81