OAI/Probability/UnimodularPercolation/Criticality/Finiteness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Critical two-cluster estimates, finite opening and almost-sure finite clusters.

  1. theorem OAI.Percolation.critical_twoLarge_probability_bound line 35
  2. theorem OAI.Percolation.critical_adjacent_infinite_connected line 56
  3. theorem OAI.Percolation.measure_union_finset_null line 119
  4. theorem OAI.Percolation.ae_union_finset line 153
  5. theorem OAI.Percolation.atMostOne_of_finite_openings line 161
  6. theorem OAI.Percolation.twoPoint_mul_le line 212
  7. theorem OAI.Percolation.reachBall_add_split line 221
  8. theorem OAI.Percolation.twoPoint_lower_on_multiples line 237
  9. theorem OAI.Percolation.reachBall_exponential_growth line 257
  10. theorem OAI.Percolation.exists_subcritical_ball_lower line 292
  11. theorem OAI.Percolation.no_uniform_positive_twoPoint_critical line 324
  12. theorem OAI.Percolation.not_unique_infinite_cluster_critical line 355
  13. theorem OAI.Percolation.critical_finite_of_transport line 392