OAI/Probability/FreeIsing/Trees/PercolationFiniteness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.SubcriticalClusters.openCluster line 14
  2. lemma OAI.Problem367.SubcriticalClusters.reachable_iff_common_downwardOpen line 18
  3. lemma OAI.Problem367.SubcriticalClusters.measurableSet_mem_openCluster line 30
  4. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_openClusters line 44
  5. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_openClusters_of_cylinder_bound line 51
  6. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_openClusters_of_survival_bound line 64
  7. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_reachable_of_incoming_cylinder_bound line 80
  8. theorem OAI.Problem367.SubcriticalClusters.finite_downwardOpen_of_nonroot line 111
  9. theorem OAI.Problem367.SubcriticalClusters.ae_all_finite_openClusters_of_nonroot_survival_bound line 142