OAI/Probability/CriticalPercolation/Modular/PeakRatioTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.one_le_modularClusterMass line 16
2. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_eq_one_of_peaks line 22
3. def OAI.CriticalPercolation.BondGraph.peakRatioTransport line 30
4. def OAI.CriticalPercolation.BondGraph.clusterPeakRatio line 35
5. lemma OAI.CriticalPercolation.BondGraph.measurable_peakRatioTransport line 38
6. lemma OAI.CriticalPercolation.BondGraph.peakRatioTransport_aut line 47
7. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_eq_zero_of_heavy line 55
8. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_eq_inv_mass line 67
9. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_le_one line 88
10. lemma OAI.CriticalPercolation.BondGraph.peakRatioTransport_incoming line 98