OAI/Probability/UnimodularPercolation/ProductMeasure/Association.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Association, disjoint witnesses and the BK inequality.

  1. theorem OAI.Percolation.bernoulli_atom_product line 19
  2. theorem OAI.Percolation.bernoulli_atom_modular line 25
  3. theorem OAI.Percolation.association_finite line 35
  4. theorem OAI.Percolation.association_events_finite line 47
  5. theorem OAI.Percolation.measurable_set_restrict line 74
  6. theorem OAI.Percolation.law_map_restrict line 80
  7. def OAI.Percolation.FiniteWitness line 99
  8. theorem OAI.Percolation.association_restricted line 102
  9. def OAI.Percolation.edgeExhaustion line 127
  10. theorem OAI.Percolation.edgeExhaustion_mono line 130
  11. theorem OAI.Percolation.subset_edgeExhaustion line 136
  12. theorem OAI.Percolation.witness_eq_union line 143
  13. theorem OAI.Percolation.association_finiteWitness line 158
  14. theorem OAI.Percolation.measurableSet_finiteWitness line 191
  15. theorem OAI.Percolation.finiteWitness_conn line 211
  16. theorem OAI.Percolation.finiteWitness_conn_finset line 223
  17. def OAI.Percolation.clusterLarge line 239
  18. theorem OAI.Percolation.clusterLarge_upper line 242
  19. theorem OAI.Percolation.finiteWitness_clusterLarge line 247
  20. theorem OAI.Percolation.measurableSet_clusterLarge line 253
  21. theorem OAI.Percolation.clusterLarge_antitone line 257
  22. theorem OAI.Percolation.infinite_cluster_eq_iInter line 262
  23. theorem OAI.Percolation.measurableSet_infinite_cluster line 276
  24. theorem OAI.Percolation.association_decreasing line 282
  25. theorem OAI.Percolation.association_infinite_cluster line 304
  26. theorem OAI.Percolation.measurable_set_preimage line 322
  27. theorem OAI.Percolation.law_map_preimage_equiv line 328
  28. theorem OAI.Percolation.isAut_symm line 347
  29. theorem OAI.Percolation.conn_aut line 354
  30. theorem OAI.Percolation.conn_aut_iff line 363
  31. theorem OAI.Percolation.cluster_aut line 376
  32. theorem OAI.Percolation.infinite_cluster_aut line 388
  33. theorem OAI.Percolation.finite_open_probability line 403
  34. theorem OAI.Percolation.twoPoint_pos line 418
  35. theorem OAI.Percolation.association_infinite_conn line 435
  36. theorem OAI.Percolation.survival_pos_of_survival_pos line 445
  37. theorem OAI.Percolation.exists_infinite_cluster_iff line 456
  38. theorem OAI.Percolation.unique_infinite_cluster_iff line 465
  39. theorem OAI.Percolation.measurableSet_unique_infinite_cluster line 479
  40. theorem OAI.Percolation.uniform_survival_pos line 493
  41. theorem OAI.Percolation.not_operatorBounded_of_unique line 520
  42. theorem OAI.Percolation.ptwo_le_pu line 547
  43. def OAI.Percolation.DisjointOccurrence line 564
  44. theorem OAI.Percolation.disjointOccurrence_upper line 568
  45. theorem OAI.Percolation.finiteWitness_disjointOccurrence line 572
  46. theorem OAI.Percolation.disjointOccurrence_mono line 580
  47. def OAI.Percolation.openSection line 586
  48. theorem OAI.Percolation.openSection_upper line 588
  49. theorem OAI.Percolation.subset_openSection line 592
  50. theorem OAI.Percolation.openSection_disjointOccurrence line 596
  51. def OAI.Percolation.finiteProbability line 629
  52. theorem OAI.Percolation.finiteProbability_nonneg line 633
  53. theorem OAI.Percolation.finiteProbability_mono line 641
  54. theorem OAI.Percolation.finiteProbability_union_add_inter line 651
  55. theorem OAI.Percolation.finiteProbability_empty line 660
  56. theorem OAI.Percolation.finiteProbability_insert line 664
  57. theorem OAI.Percolation.empty_mem_disjointOccurrence line 700
  58. theorem OAI.Percolation.finiteProbability_disjointOccurrence_le_half line 712
  59. theorem OAI.Percolation.finiteProbability_univ line 768
  60. theorem OAI.Percolation.disjointOccurrence_image line 787
  61. theorem OAI.Percolation.bk_finite_half line 823
  62. theorem OAI.Percolation.bk_restricted_half line 829
  63. theorem OAI.Percolation.bk_finiteWitness_half line 857
  64. def OAI.Percolation.orParameter line 881
  65. abbrev OAI.Percolation.bitLaw line 886
  66. instance OAI.Percolation.bitLaw_isProbabilityMeasure line 890
  67. theorem OAI.Percolation.map_nonempty line 895
  68. theorem OAI.Percolation.finite_image_lift line 928
  69. theorem OAI.Percolation.finiteWitness_image_preimage line 936
  70. theorem OAI.Percolation.image_preimage_disjointOccurrence line 943
  71. theorem OAI.Percolation.map_exists_bitLaw line 963
  72. theorem OAI.Percolation.measurable_image_fst line 972
  73. theorem OAI.Percolation.law_map_image_fst line 992
  74. theorem OAI.Percolation.exists_orParameter line 1020
  75. theorem OAI.Percolation.disjointOccurrence_subset_inter line 1044
  76. theorem OAI.Percolation.bk line 1051