OAI/Probability/CriticalPercolation/Criticality/ContractingDomains.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.modularRatio_aut_weight line 17
2. lemma OAI.CriticalPercolation.BondGraph.exists_weight_contraction line 24
3. lemma OAI.CriticalPercolation.BondGraph.uniform_weight_contraction line 53
4. def OAI.CriticalPercolation.BondGraph.safeBallDomain line 84
5. lemma OAI.CriticalPercolation.BondGraph.safeBallDomain_mono line 88
6. lemma OAI.CriticalPercolation.BondGraph.safeBallDomain_subset line 92
7. lemma OAI.CriticalPercolation.BondGraph.modularRatio_ball_upper line 97
8. lemma OAI.CriticalPercolation.BondGraph.safeBallDomain_low_inclusion line 110
9. def OAI.CriticalPercolation.BondGraph.InsideWalk line 127
10. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.mono line 130
11. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.refl line 136
12. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.reverse line 143
13. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.append line 150
14. lemma OAI.CriticalPercolation.BondGraph.insideWalk_ball line 159
15. lemma OAI.CriticalPercolation.BondGraph.modularRatio_weight_pow line 167
16. lemma OAI.CriticalPercolation.BondGraph.safeBallDomain_iterate line 179
17. theorem OAI.CriticalPercolation.BondGraph.safeBallDomain_uniform_descent line 215