OAI/Probability/UnimodularPercolation/Graph/Basic.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Percolation.BondGraph line 14

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:12 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:14 (same declaration text).

2. def OAI.Percolation.Adj line 17

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:14 (same declaration text).

3. def OAI.Percolation.LocallyFinite line 20

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:16 (same declaration text).

4. def OAI.Percolation.Connected line 23

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:18 (same declaration text).

5. def OAI.Percolation.IsAut line 27

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:21 (same declaration text).

6. def OAI.Percolation.QuasiTransitive line 31

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:24 (same declaration text).

7. def OAI.Percolation.vertexBoundary line 36

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:28 (same declaration text).

8. def OAI.Percolation.hV line 40

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:31 (same declaration text).

9. def OAI.Percolation.Conn line 45

   Also declared: ComparatorChallenges/BenjaminiSchramm.lean:35 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:16 (same declaration text).

10. def OAI.Percolation.cluster line 48

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:38 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:19 (same declaration text).

11. def OAI.Percolation.infiniteClusters line 52

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:41 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:22 (same declaration text).

12. def OAI.Percolation.law line 56

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:44 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:25 (same declaration text).

13. def OAI.Percolation.pc line 59

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:47 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:28 (same declaration text).

14. def OAI.Percolation.pu line 62

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:50 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:31 (same declaration text).

15. def OAI.Percolation.twoPoint line 65

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:53 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:34 (same declaration text).

16. abbrev OAI.Percolation.Hilbert line 68

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:56 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:37 (same declaration text).

17. def OAI.Percolation.HasKernel line 71

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:58 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:39 (same declaration text).

18. def OAI.Percolation.OperatorBounded line 76

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:63 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:44 (same declaration text).

19. def OAI.Percolation.operatorNorm line 81

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:67 (same declaration text).

20. def OAI.Percolation.ptwo line 86

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:72 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:48 (same declaration text).

21. def OAI.Percolation.labelLaw line 90

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:75 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:51 (same declaration text).

22. def OAI.Percolation.openEdges line 93

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:78 (same declaration text), ComparatorChallenges/CayleyPercolation.lean:54 (same declaration text).

23. def OAI.Percolation.MainConclusion line 97

    Also declared: ComparatorChallenges/BenjaminiSchramm.lean:81 (same declaration text).

24. theorem OAI.Percolation.conn_refl line 111
25. theorem OAI.Percolation.conn_trans line 114
26. theorem OAI.Percolation.conn_symm line 117
27. theorem OAI.Percolation.conn_mono line 124
28. theorem OAI.Percolation.cluster_eq_of_conn line 130
29. theorem OAI.Percolation.mem_cluster_self line 136
30. theorem OAI.Percolation.clusters_eq_or_disjoint line 138
31. theorem OAI.Percolation.conn_empty_iff line 147
32. theorem OAI.Percolation.cluster_empty line 156
33. theorem OAI.Percolation.infiniteClusters_empty line 160
34. theorem OAI.Percolation.conn_univ_of_connected line 168
35. theorem OAI.Percolation.cluster_univ_of_connected line 173
36. theorem OAI.Percolation.infiniteClusters_univ line 179
37. instance OAI.Percolation.law_isProbabilityMeasure line 196
38. theorem OAI.Percolation.law_zero line 201
39. theorem OAI.Percolation.law_one line 204
40. theorem OAI.Percolation.twoPoint_self line 207
41. theorem OAI.Percolation.twoPoint_nonneg line 210
42. theorem OAI.Percolation.twoPoint_le_one line 213
43. theorem OAI.Percolation.twoPoint_symm line 217
44. theorem OAI.Percolation.twoPoint_zero line 223
45. theorem OAI.Percolation.twoPoint_one line 231
46. theorem OAI.Percolation.kernel_extension_unique line 245
47. theorem OAI.Percolation.HasKernel.unique line 262
48. theorem OAI.Percolation.operatorNorm_of_hasKernel line 267
49. theorem OAI.Percolation.operatorNorm_eq_top_iff line 282
50. theorem OAI.Percolation.operatorNorm_lt_top_iff line 298
51. theorem OAI.Percolation.hasKernel_zero line 302
52. theorem OAI.Percolation.operatorBounded_zero line 311
53. theorem OAI.Percolation.finite_neighbors line 319
54. def OAI.Percolation.reachBall line 334
55. theorem OAI.Percolation.finite_reachBall line 338
56. theorem OAI.Percolation.exists_mem_reachBall line 346
57. theorem OAI.Percolation.countable_vertices line 356
58. theorem OAI.Percolation.countable_edges line 367