OAI/Probability/UnimodularPercolation/Criticality/Connectivity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Critical connection probabilities and nonamenable growth.

  1. theorem OAI.Percolation.connectivity_twoPoint_mul_le line 17
  2. theorem OAI.Percolation.reachBall_split line 27
  3. theorem OAI.Percolation.twoPoint_block_lower line 45
  4. theorem OAI.Percolation.isoperimetric_ball_growth line 64
  5. theorem OAI.Percolation.subcritical_block_bound line 97
  6. theorem OAI.Percolation.uniform_ball_lower_below line 125
  7. theorem OAI.Percolation.critical_twoPoint_no_uniform_positive line 153
  8. theorem OAI.Percolation.critical_not_ae_unique line 166