OAI/Probability/BenjaminiSchramm/GhostTiltedTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.ghostAvoid line 11
2. lemma OAI.Percolation.BenjaminiSchramm.measurable_ghostAvoid line 14
3. lemma OAI.Percolation.BenjaminiSchramm.ghostAvoid_antitone line 18
4. def OAI.CriticalPercolation.BondGraph.ghostHighTransport line 35
5. lemma OAI.CriticalPercolation.BondGraph.measurable_ghostHighTransport line 40
6. lemma OAI.CriticalPercolation.BondGraph.ghostHighTransport_aut line 45
7. lemma OAI.CriticalPercolation.BondGraph.ghostHighTransport_incoming_le line 53
8. theorem OAI.CriticalPercolation.BondGraph.ghostHighTransport_expected_le line 91
9. def OAI.CriticalPercolation.BondGraph.ghostWeightedCount line 104
10. lemma OAI.CriticalPercolation.BondGraph.ghostWeightedCount_le line 108
11. theorem OAI.CriticalPercolation.BondGraph.expected_ghostWeightedCount_le line 126