OAI/Probability/BenjaminiSchramm/GhostBondBK.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Percolation.BenjaminiSchramm.finiteGhostConnectionline 14 - lemma
OAI.Percolation.BenjaminiSchramm.finiteGhostConnection_upperline 17 - lemma
OAI.Percolation.BenjaminiSchramm.finiteGhostConnection_finiteWitnessline 21 - theorem
OAI.Percolation.BenjaminiSchramm.finiteGhostConnection_bkline 27 - theorem
OAI.Percolation.BenjaminiSchramm.averaged_finiteGhostConnection_bkline 35 - lemma
OAI.Percolation.BenjaminiSchramm.measurable_finiteGhostConnection_measureline 51 - theorem
OAI.Percolation.BenjaminiSchramm.averaged_ghostConnection_bkline 64 - lemma
OAI.Percolation.BenjaminiSchramm.measurableSet_ghostDisjointOccurrenceline 85