OAI/Probability/CriticalPercolation/Modular/PeakVolumeBand.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.peakVolumeBand line 15
2. lemma OAI.CriticalPercolation.BondGraph.measurable_peakVolumeBand line 19
3. lemma OAI.CriticalPercolation.BondGraph.peakVolumeBand_le_one line 26
4. lemma OAI.CriticalPercolation.BondGraph.peakVolumeBand_support line 32
5. lemma OAI.CriticalPercolation.BondGraph.peakVolumeBand_mul_le line 51
6. theorem OAI.CriticalPercolation.BondGraph.expected_peakVolumeBand_mul_le line 59