OAI/Probability/BenjaminiSchramm/GhostField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.ghostRate line 12
2. def OAI.Percolation.BenjaminiSchramm.ghostFieldLaw line 15
3. instance OAI.Percolation.BenjaminiSchramm.ghostFieldLaw_probability line 18
4. lemma OAI.Percolation.BenjaminiSchramm.ghostRate_closed_probability line 23
5. theorem OAI.Percolation.BenjaminiSchramm.ghostFieldLaw_avoid_finset line 32
6. theorem OAI.Percolation.BenjaminiSchramm.ghostFieldLaw_avoid_finite line 65
7. def OAI.Percolation.BenjaminiSchramm.ghostHits line 72
8. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_ghostHits line 74
9. lemma OAI.Percolation.BenjaminiSchramm.ghostHits_compl line 78
10. theorem OAI.Percolation.BenjaminiSchramm.ghostFieldLaw_real_hit_finset line 82
11. theorem OAI.Percolation.BenjaminiSchramm.twoGhostFieldLaw_real_hit_finset line 93