OAI/Probability/BenjaminiSchramm/ExponentialDecay.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Percolation.BenjaminiSchramm.walk_crosses_sphere line 16
2. theorem OAI.Percolation.BenjaminiSchramm.mem_reachBall_of_graphDistance_le line 30
3. theorem OAI.Percolation.BenjaminiSchramm.sphere_split_subset line 40
4. theorem OAI.Percolation.BenjaminiSchramm.twoPoint_le_sphere_sum line 63
5. theorem OAI.Percolation.BenjaminiSchramm.connectivity_power_lower line 84
6. theorem OAI.Percolation.BenjaminiSchramm.connectivity_block_bound line 148
7. theorem OAI.Percolation.BenjaminiSchramm.connectivity_exponential_bound line 169
8. theorem OAI.Percolation.BenjaminiSchramm.exponentialDecay_of_bounded line 223
9. theorem OAI.Percolation.BenjaminiSchramm.exponentialDecay_of_lt_ptwo line 232
10. theorem OAI.Percolation.BenjaminiSchramm.ptwo_le_pexp line 239