OAI/Probability/CriticalPercolation/Modular/PeakReturn.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.peakReturn line 16
  2. lemma OAI.CriticalPercolation.BondGraph.measurable_peakReturn line 19
  3. lemma OAI.CriticalPercolation.BondGraph.peakReturn_eq_inv_ncard line 27
  4. lemma OAI.CriticalPercolation.BondGraph.peakReturn_le_one line 33
  5. lemma OAI.CriticalPercolation.BondGraph.peakRatioTransport_incoming_ae line 42
  6. theorem OAI.CriticalPercolation.BondGraph.expected_clusterPeakRatio line 59
  7. lemma OAI.CriticalPercolation.BondGraph.clusterPeak_of_subset line 73
  8. lemma OAI.CriticalPercolation.BondGraph.eventually_cluster_of_exhaustion line 77
  9. lemma OAI.CriticalPercolation.BondGraph.eventually_peaks_of_exhaustion line 88
  10. lemma OAI.CriticalPercolation.BondGraph.tendsto_peakCount_of_exhaustion line 95
  11. lemma OAI.CriticalPercolation.BondGraph.tendsto_peakReturn_of_exhaustion line 111