OAI/Probability/BenjaminiSchramm/GhostPivotalProbability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Percolation.BenjaminiSchramm.criticalModel_eraseVertices line 16
2. lemma OAI.Percolation.BenjaminiSchramm.force_closed_eq_sdiff line 30
3. lemma OAI.Percolation.BenjaminiSchramm.measurableSet_ghostBridge_fixed_cluster line 35
4. theorem OAI.Percolation.BenjaminiSchramm.ghostBridge_fixed_cluster_measure_le line 47
5. theorem OAI.Percolation.BenjaminiSchramm.averaged_ghostBridge_fixed_cluster_le line 113