OAI/Probability/CriticalPercolation/Exploration/ClusterUsers.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalPercolation.ExactExposure.pair_transcript_incidence line 26
  2. def OAI.CriticalPercolation.ExactExposure.clusterUsers line 40
  3. lemma OAI.CriticalPercolation.ExactExposure.pair_users line 45
  4. lemma OAI.CriticalPercolation.ExactExposure.pair_overlap_four line 61
  5. theorem OAI.CriticalPercolation.ExactExposure.pair_entropy line 69
  6. theorem OAI.CriticalPercolation.ExactExposure.pair_transcript_left_cluster line 84
  7. lemma OAI.CriticalPercolation.ExactExposure.pair_transcript_right_cluster line 95
  8. def OAI.CriticalPercolation.ExactExposure.configuration line 113
  9. def OAI.CriticalPercolation.ExactExposure.Admissible line 115
  10. lemma OAI.CriticalPercolation.ExactExposure.admissible_closed line 120
  11. lemma OAI.CriticalPercolation.ExactExposure.admissible_congr line 128
  12. theorem OAI.CriticalPercolation.ExactExposure.pair_contact_prices line 139
  13. def OAI.CriticalPercolation.ExactExposure.markWeight line 163
  14. def OAI.CriticalPercolation.ExactExposure.markCost line 170
  15. lemma OAI.CriticalPercolation.ExactExposure.pair_mark_congr line 178