OAI/Probability/FreeIsing/Trees/SubcriticalClusters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.SubcriticalClusters.DownwardOpen line 15
2. def OAI.Problem367.SubcriticalClusters.pathCoordinates line 20
3. lemma OAI.Problem367.SubcriticalClusters.mem_pathCoordinates line 23
4. lemma OAI.Problem367.SubcriticalClusters.card_pathCoordinates line 30
5. lemma OAI.Problem367.SubcriticalClusters.uniform01_Iic line 40
6. lemma OAI.Problem367.SubcriticalClusters.path_open_mass line 48
7. lemma OAI.Problem367.SubcriticalClusters.downwardOpen_mass_le line 68
8. theorem OAI.Problem367.SubcriticalClusters.ae_finite_of_depth_bound line 75
9. theorem OAI.Problem367.SubcriticalClusters.ae_finite_downwardOpen line 118
10. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_downwardOpen line 129
11. lemma OAI.Problem367.SubcriticalClusters.pathCoordinates_ne_nil line 135
12. lemma OAI.Problem367.SubcriticalClusters.path_event_eq_cylinder line 143
13. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_downwardOpen_of_cylinder_bound line 156
14. lemma OAI.Problem367.SubcriticalClusters.measurableSet_downwardOpen line 184