OAI/Probability/UnimodularPercolation/TwoCluster/Bounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Quantitative two-cluster probability bounds.

  1. theorem OAI.Percolation.localDensityLoss_integral_bound line 18
  2. theorem OAI.Percolation.cluster_insert_left_eq_union line 65
  3. theorem OAI.Percolation.endpoint_density_defect line 80
  4. theorem OAI.Percolation.localDensityLoss_ge_edge line 105
  5. theorem OAI.Percolation.two_large_endpoint_loss line 114
  6. def OAI.Percolation.twoLargeEvent line 146
  7. theorem OAI.Percolation.measurableSet_twoLargeEvent line 149
  8. theorem OAI.Percolation.twoLarge_probability_bound line 154
  9. theorem OAI.Percolation.finiteWitness_eventually_iff line 193
  10. theorem OAI.Percolation.twoLarge_probability_tendsto line 211