OAI/Probability/FreeIsing/Trees/PercolationSurvival.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.SubcriticalClusters.takeVertex_takeVertex line 13
2. lemma OAI.Problem367.SubcriticalClusters.DownwardOpen.take line 20
3. def OAI.Problem367.SubcriticalClusters.survivalEvent line 33
4. lemma OAI.Problem367.SubcriticalClusters.survivalEvent_antitone line 37
5. lemma OAI.Problem367.SubcriticalClusters.measurableSet_survivalEvent line 47
6. lemma OAI.Problem367.SubcriticalClusters.finite_downwardOpen_iff line 58
7. lemma OAI.Problem367.SubcriticalClusters.infinite_downwardOpen_iff_survives line 81
8. theorem OAI.Problem367.SubcriticalClusters.ae_finite_downwardOpen_of_survival_tendsto_zero line 88
9. theorem OAI.Problem367.SubcriticalClusters.ae_finite_downwardOpen_of_survival_bound line 101