OAI/Probability/BenjaminiSchramm/GhostEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Percolation.BenjaminiSchramm.markedConnection_entropy_comparison line 15
2. theorem OAI.Percolation.BenjaminiSchramm.finiteClusterTail_eq_restricted_volume line 44
3. theorem OAI.Percolation.BenjaminiSchramm.finiteWitness_restricted_probability_tendsto line 74
4. theorem OAI.Percolation.BenjaminiSchramm.volumeEvent_upper line 86
5. theorem OAI.Percolation.BenjaminiSchramm.volumeEvent_finiteWitness line 91
6. theorem OAI.Percolation.BenjaminiSchramm.volume_probability_le_of_finite_tails line 96
7. theorem OAI.Percolation.BenjaminiSchramm.percolationProbability_le_of_marked_bounds line 108