OAI/Probability/CriticalPercolation/Entropy/BinaryPairs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CriticalPercolation.BinaryLaw.active_cluster_users_le line 16
2. abbrev OAI.CriticalPercolation.BinaryLaw.ActiveIndex line 66
3. def OAI.CriticalPercolation.BinaryLaw.activeLeft line 68
4. def OAI.CriticalPercolation.BinaryLaw.activeRight line 71
5. lemma OAI.CriticalPercolation.BinaryLaw.fixed_cluster_users_le line 75
6. lemma OAI.CriticalPercolation.BinaryLaw.configurationMass_support line 105
7. theorem OAI.CriticalPercolation.BinaryLaw.conditioned_pair_entropy line 123