OAI/Probability/BenjaminiSchramm/PeakHalfspaceTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.adjustedHalfspaceConn_aut line 13
2. lemma OAI.CriticalPercolation.BondGraph.adjustedStrictHalfspacePeak_aut line 30
3. lemma OAI.CriticalPercolation.BondGraph.strictPeakBandTransport_aut line 47
4. lemma OAI.CriticalPercolation.BondGraph.measurable_adjustedHalfspaceConn line 57
5. lemma OAI.CriticalPercolation.BondGraph.measurable_adjustedStrictHalfspacePeak line 64
6. lemma OAI.CriticalPercolation.BondGraph.measurable_strictPeakBandTransport line 69
7. lemma OAI.CriticalPercolation.BondGraph.measurable_strictPeakSlabBandTransport line 75
8. lemma OAI.CriticalPercolation.BondGraph.measurable_strictPeakSlabBandCount line 84
9. theorem OAI.CriticalPercolation.BondGraph.expected_strictPeakSlabBandCount_bound line 88