OAI/Probability/UnimodularPercolation/Clusters/Uniqueness.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Cluster events, invariant covers and uniqueness thresholds.

  1. def OAI.Percolation.vertexOrbit line 18
  2. theorem OAI.Percolation.adj_aut line 21
  3. theorem OAI.Percolation.mem_reachBall_aut line 26
  4. theorem OAI.Percolation.vertexOrbit_infinite line 42
  5. def OAI.Percolation.deltaSum line 63
  6. theorem OAI.Percolation.deltaSum_apply line 65
  7. theorem OAI.Percolation.inner_deltaSum line 70
  8. theorem OAI.Percolation.norm_deltaSum_sq line 74
  9. theorem OAI.Percolation.sum_twoPoint_le_norm_card line 84
  10. theorem OAI.Percolation.card_sq_le_image_card_mul_pairs line 112
  11. theorem OAI.Percolation.square_sum_probability_le line 152
  12. theorem OAI.Percolation.cluster_eq_iff_conn line 194
  13. def OAI.Percolation.TouchedCover line 203
  14. theorem OAI.Percolation.measurableSet_touchedCover line 208
  15. theorem OAI.Percolation.survivor_count_sq_le line 227
  16. theorem OAI.Percolation.labelLaw_map_precomp line 264
  17. theorem OAI.Percolation.infinite_cluster_precomp line 276
  18. theorem OAI.Percolation.touchedCover_precomp line 287
  19. theorem OAI.Percolation.cover_survival_aut line 302
  20. theorem OAI.Percolation.cover_survival_square_sum_le line 329
  21. theorem OAI.Percolation.measure_cover_survival_eq_zero line 368
  22. theorem OAI.Percolation.cluster_union_subset line 402
  23. theorem OAI.Percolation.exists_infinite_cluster_mono line 421
  24. theorem OAI.Percolation.exists_infinite_cluster_sdiff line 427
  25. theorem OAI.Percolation.infiniteClusters_nonempty_iff line 453
  26. theorem OAI.Percolation.measurableSet_exists_infinite_cluster line 461
  27. theorem OAI.Percolation.infinite_cluster_zero_one line 465
  28. theorem OAI.Percolation.exists_infinite_cluster_probability_mono line 520
  29. theorem OAI.Percolation.ae_exists_infinite_cluster_of_pc_lt line 534
  30. theorem OAI.Percolation.touchedCover_of_finite_infiniteClusters line 550
  31. theorem OAI.Percolation.coupled_interval line 574