OAI/Probability/CriticalPercolation/Modular/HeavyThinning.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_aut line 19
  2. def OAI.CriticalPercolation.BondGraph.heavyFlag line 25
  3. lemma OAI.CriticalPercolation.BondGraph.measurable_heavyFlag line 28
  4. lemma OAI.CriticalPercolation.BondGraph.heavyFlag_iff_of_reachable line 33
  5. lemma OAI.CriticalPercolation.BondGraph.heavyFlag_aut line 42
  6. def OAI.CriticalPercolation.BondGraph.heavyRestrictedPeakTransport line 47
  7. lemma OAI.CriticalPercolation.BondGraph.measurable_heavyRestrictedPeakTransport line 50
  8. lemma OAI.CriticalPercolation.BondGraph.heavyRestrictedPeakTransport_aut line 56
  9. lemma OAI.CriticalPercolation.BondGraph.heavyRestrictedPeakTransport_out line 63
  10. lemma OAI.CriticalPercolation.BondGraph.heavyRestrictedPeakTransport_swap line 70
  11. lemma OAI.CriticalPercolation.BondGraph.heavyRestrictedPeakTransport_incoming_ae line 78
  12. lemma OAI.CriticalPercolation.BondGraph.expected_heavy_clusterPeakRatio line 90
  13. lemma OAI.CriticalPercolation.BondGraph.tendsto_expected_heavy_peakReturn line 105
  14. theorem OAI.CriticalPercolation.BondGraph.tendsto_sum_expected_heavy_clusterPeakRatio line 137