OAI/Probability/BenjaminiSchramm/PeakLayerEstimate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.boundedPeakTransport line 13
2. def OAI.CriticalPercolation.BondGraph.boundedPeakMass line 16
3. lemma OAI.CriticalPercolation.BondGraph.measurable_boundedPeakTransport line 19
4. lemma OAI.CriticalPercolation.BondGraph.boundedPeakTransport_aut line 25
5. lemma OAI.CriticalPercolation.BondGraph.boundedPeakTransport_outgoing line 32
6. lemma OAI.CriticalPercolation.BondGraph.boundedPeakTransport_incoming line 47
7. theorem OAI.CriticalPercolation.BondGraph.expected_boundedPeakMass_sum line 70
8. lemma OAI.CriticalPercolation.BondGraph.measurable_boundedPeakMass line 92
9. lemma OAI.CriticalPercolation.BondGraph.boundedPeakMass_aut line 98
10. theorem OAI.CriticalPercolation.BondGraph.expected_boundedPeakMass line 103
11. def OAI.CriticalPercolation.BondGraph.boundedPeakUpperLayerCount line 118
12. lemma OAI.CriticalPercolation.BondGraph.measurable_boundedPeakUpperLayerCount line 123
13. lemma OAI.CriticalPercolation.BondGraph.weighted_boundedPeakUpperLayerCount line 133
14. theorem OAI.CriticalPercolation.BondGraph.expected_boundedPeakUpperLayerCount line 148