OAI/Probability/CriticalPercolation/Modular/WeightedPeakTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_eq_of_reachable line 16
2. lemma OAI.CriticalPercolation.BondGraph.measurable_clusterPeakRatio line 21
3. lemma OAI.CriticalPercolation.BondGraph.Aut.clusterPeakRatio line 25
4. lemma OAI.CriticalPercolation.BondGraph.weighted_peakRatio_incoming line 33
5. theorem OAI.CriticalPercolation.BondGraph.expected_weighted_peakRatio line 45
6. def OAI.CriticalPercolation.BondGraph.normalizedClusterVolume line 65
7. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedClusterVolume line 68
8. lemma OAI.CriticalPercolation.BondGraph.Aut.normalizedClusterVolume line 75
9. lemma OAI.CriticalPercolation.BondGraph.normalizedClusterVolume_eq_of_reachable line 80
10. lemma OAI.CriticalPercolation.BondGraph.normalizedClusterVolume_eq_at_peak line 86
11. lemma OAI.CriticalPercolation.BondGraph.normalizedClusterVolume_mul_ratio_le line 92
12. theorem OAI.CriticalPercolation.BondGraph.expected_peak_volume_le line 101