OAI/Probability/CriticalPercolation/Criticality/ActualGrowth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.Corridor.Scheme.actual line 18
2. lemma OAI.CriticalPercolation.Corridor.Scheme.actual_succ line 20
3. lemma OAI.CriticalPercolation.Corridor.Scheme.actual_good_mono line 24
4. lemma OAI.CriticalPercolation.Corridor.Scheme.actual_root line 30
5. def OAI.CriticalPercolation.Corridor.Scheme.allGood line 33
6. lemma OAI.CriticalPercolation.Corridor.Scheme.allGood_root line 35
7. lemma OAI.CriticalPercolation.Corridor.Scheme.allGood_quadrant line 37
8. lemma OAI.CriticalPercolation.Corridor.Scheme.actual_good_birth line 41
9. lemma OAI.CriticalPercolation.Corridor.Scheme.good_parent_present line 60
10. lemma OAI.CriticalPercolation.Corridor.Scheme.missing_child_fails line 71
11. lemma OAI.CriticalPercolation.Corridor.Scheme.allGood_reached line 108