OAI/Probability/CriticalPercolation/Entropy/BinaryForest.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BinaryLaw.nodeParent line 15
  2. lemma OAI.CriticalPercolation.BinaryLaw.nodeParent_lt line 23
  3. def OAI.CriticalPercolation.BinaryLaw.historyForest line 37
  4. lemma OAI.CriticalPercolation.BinaryLaw.nodeParent_old line 41
  5. def OAI.CriticalPercolation.BinaryLaw.node line 45
  6. lemma OAI.CriticalPercolation.BinaryLaw.node_old line 48
  7. lemma OAI.CriticalPercolation.BinaryLaw.node_current line 54
  8. lemma OAI.CriticalPercolation.BinaryLaw.node_getElem? line 60
  9. lemma OAI.CriticalPercolation.BinaryLaw.node_mem line 65
  10. lemma OAI.CriticalPercolation.BinaryLaw.node_bases line 68
  11. lemma OAI.CriticalPercolation.BinaryLaw.nodeParent_current line 81
  12. lemma OAI.CriticalPercolation.BinaryLaw.node_colour_parent line 91
  13. lemma OAI.CriticalPercolation.BinaryLaw.node_root_colour line 112
  14. def OAI.CriticalPercolation.BinaryLaw.Canonical line 129
  15. lemma OAI.CriticalPercolation.BinaryLaw.parent_canonical line 133
  16. lemma OAI.CriticalPercolation.BinaryLaw.canonical_append line 150
  17. lemma OAI.CriticalPercolation.BinaryLaw.canonical_distinct line 157
  18. lemma OAI.CriticalPercolation.BinaryLaw.nodeParent_canonical line 171
  19. lemma OAI.CriticalPercolation.BinaryLaw.lineage_canonical line 193
  20. def OAI.CriticalPercolation.BinaryLaw.owner line 213
  21. lemma OAI.CriticalPercolation.BinaryLaw.owner_exists line 216
  22. lemma OAI.CriticalPercolation.BinaryLaw.owner_lt line 223
  23. lemma OAI.CriticalPercolation.BinaryLaw.owner_canonical line 229
  24. lemma OAI.CriticalPercolation.BinaryLaw.owner_reachable line 234
  25. lemma OAI.CriticalPercolation.BinaryLaw.owner_colour line 242
  26. lemma OAI.CriticalPercolation.BinaryLaw.terminal_roots line 252