OAI/Probability/BenjaminiSchramm/ProbabilityLower.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Percolation.BenjaminiSchramm.cluster_finite_ae_of_finite_mass line 14
2. theorem OAI.Percolation.BenjaminiSchramm.uniform_testSets_of_good_cost line 32
3. theorem OAI.Percolation.BenjaminiSchramm.finite_mass_of_uniform_testSets line 55
4. theorem OAI.Percolation.BenjaminiSchramm.exists_bad_cost_of_pc_lt line 79
5. theorem OAI.Percolation.BenjaminiSchramm.percolationProbability_mul_twoPoint_le line 101
6. theorem OAI.Percolation.BenjaminiSchramm.percolationProbability_lower_of_bad_cost line 110
7. theorem OAI.Percolation.BenjaminiSchramm.one_sub_exp_neg_linear line 125
8. theorem OAI.Percolation.BenjaminiSchramm.percolationProbability_linear_lower line 133