OAI/Probability/BenjaminiSchramm/ExteriorEscape.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.exteriorEscape line 13
2. lemma OAI.Percolation.BenjaminiSchramm.exteriorEscape_upper line 16
3. lemma OAI.Percolation.BenjaminiSchramm.exteriorEscape_hasFiniteOpenWitness line 21
4. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_exteriorEscape line 29
5. lemma OAI.Percolation.BenjaminiSchramm.conn_eq_of_incident_closed line 34
6. lemma OAI.Percolation.BenjaminiSchramm.finiteBondPattern_excludes_exteriorEscape line 43
7. lemma OAI.CriticalPercolation.BernoulliProduct.finiteBondPattern_law_eq_of_parameters line 60
8. lemma OAI.CriticalPercolation.BernoulliProduct.finiteBondPattern_inhomogeneous_lower line 83
9. theorem OAI.Percolation.BenjaminiSchramm.exteriorEscape_avoidance_finite_energy line 96
10. theorem OAI.Percolation.BenjaminiSchramm.exteriorEscape_avoidance_product line 106