OAI/Probability/BenjaminiSchramm/PeakFirstMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.normalizedPeakTransport line 13
2. lemma OAI.CriticalPercolation.BondGraph.normalizedPeakTransport_aut line 16
3. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedPeakTransport line 23
4. lemma OAI.CriticalPercolation.BondGraph.normalizedPeakTransport_outgoing line 31
5. lemma OAI.CriticalPercolation.BondGraph.normalizedPeakTransport_incoming line 41
6. lemma OAI.CriticalPercolation.BondGraph.normalizedPeakTransport_eq_reverse line 61
7. theorem OAI.CriticalPercolation.BondGraph.expected_peakReturn_modularMass_sum line 75