OAI/Probability/CriticalPercolation/GraphGeometry/VertexBall.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalPercolation.BondGraph.openGraph_mono line 14
  2. theorem OAI.CriticalPercolation.BondGraph.cluster_mono line 18
  3. theorem OAI.CriticalPercolation.BondGraph.percolates_mono line 22
  4. theorem OAI.CriticalPercolation.BondGraph.finite_neighbors line 27
  5. def OAI.CriticalPercolation.BondGraph.vertexBall line 38
  6. lemma OAI.CriticalPercolation.BondGraph.vertexBall_finite line 42
  7. lemma OAI.CriticalPercolation.BondGraph.reachable_mem_vertexBall line 48
  8. theorem OAI.CriticalPercolation.BondGraph.countable_vertices line 58
  9. theorem OAI.CriticalPercolation.BondGraph.countable_bonds line 71
  10. def OAI.CriticalPercolation.BondGraph.lengthReach line 83
  11. lemma OAI.CriticalPercolation.BondGraph.reachable_iff_exists_lengthReach line 87
  12. lemma OAI.CriticalPercolation.BondGraph.measurable_openGraph_adj line 104
  13. lemma OAI.CriticalPercolation.BondGraph.measurable_lengthReach line 110
  14. lemma OAI.CriticalPercolation.BondGraph.measurable_reachable line 117
  15. lemma OAI.CriticalPercolation.BondGraph.measurable_cluster line 122
  16. lemma OAI.CriticalPercolation.BondGraph.measurable_infinite_cluster line 126
  17. theorem OAI.CriticalPercolation.BondGraph.measurableSet_percolates line 131
  18. theorem OAI.CriticalPercolation.BondGraph.percolates_null_iff line 135
  19. lemma OAI.CriticalPercolation.BondGraph.openGraph_empty line 142
  20. lemma OAI.CriticalPercolation.BondGraph.cluster_empty line 145
  21. lemma OAI.CriticalPercolation.BondGraph.empty_not_percolates line 149
  22. lemma OAI.CriticalPercolation.BondGraph.law_zero_percolates line 152
  23. lemma OAI.CriticalPercolation.BondGraph.cluster_univ_of_connected line 157
  24. lemma OAI.CriticalPercolation.BondGraph.law_one_percolates line 161
  25. lemma OAI.CriticalPercolation.BondGraph.criticalProbability_le_of_pos line 170
  26. lemma OAI.CriticalPercolation.BondGraph.law_percolates_eq_zero_of_lt_critical line 174
  27. lemma OAI.CriticalPercolation.BondGraph.cluster_subset_endpoints line 179
  28. lemma OAI.CriticalPercolation.BondGraph.finite_cluster_of_finite_bonds line 190
  29. lemma OAI.CriticalPercolation.BondGraph.not_percolates_of_finite_bonds line 202
  30. lemma OAI.CriticalPercolation.BondGraph.mem_cluster_finite_witness line 207
  31. lemma OAI.CriticalPercolation.BondGraph.finite_subset_cluster_finite_witness line 224
  32. def OAI.CriticalPercolation.ClusterDeletion.delete line 244
  33. def OAI.CriticalPercolation.ClusterDeletion.roots line 249
  34. def OAI.CriticalPercolation.ClusterDeletion.component line 252
  35. lemma OAI.CriticalPercolation.ClusterDeletion.delete_antitone line 255
  36. lemma OAI.CriticalPercolation.ClusterDeletion.delete_le line 259
  37. lemma OAI.CriticalPercolation.ClusterDeletion.roots_mono line 262
  38. lemma OAI.CriticalPercolation.ClusterDeletion.component_mono line 267
  39. lemma OAI.CriticalPercolation.ClusterDeletion.roots_self line 271
  40. lemma OAI.CriticalPercolation.ClusterDeletion.reachable_not_mem_roots line 274
  41. lemma OAI.CriticalPercolation.ClusterDeletion.roots_closed line 279
  42. lemma OAI.CriticalPercolation.ClusterDeletion.reachable_mem_of_closed line 284
  43. lemma OAI.CriticalPercolation.ClusterDeletion.roots_subset_of_adj line 293
  44. lemma OAI.CriticalPercolation.ClusterDeletion.roots_eq_of_adj_eq_incident line 305
  45. lemma OAI.CriticalPercolation.ClusterDeletion.delete_roots_component line 316
  46. lemma OAI.CriticalPercolation.ClusterDeletion.delete_delete line 331
  47. lemma OAI.CriticalPercolation.ClusterDeletion.delete_roots_union_component line 337
  48. def OAI.CriticalPercolation.ClusterDeletion.residual line 343
  49. lemma OAI.CriticalPercolation.ClusterDeletion.residual_nonneg line 351
  50. lemma OAI.CriticalPercolation.ClusterDeletion.residual_monotone line 359
  51. def OAI.CriticalPercolation.BondGraph.incidentEdges line 380
  52. lemma OAI.CriticalPercolation.BondGraph.openGraph_adj_eq_of_incident line 382
  53. lemma OAI.CriticalPercolation.BondGraph.roots_eq_of_incident line 395
  54. lemma OAI.CriticalPercolation.BondGraph.dependsOn_exact_roots line 401
  55. lemma OAI.CriticalPercolation.BondGraph.delete_openGraph_dependsOn line 409
  56. lemma OAI.CriticalPercolation.BondGraph.deleted_roots_eq_of_incident line 436
  57. lemma OAI.CriticalPercolation.BondGraph.dependsOn_exact_deleted_roots line 446