OAI/Probability/CriticalPercolation/Entropy/BinaryWords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BinaryLaw.sides line 14
  2. def OAI.CriticalPercolation.BinaryLaw.marks line 18
  3. def OAI.CriticalPercolation.BinaryLaw.fromWords line 22
  4. lemma OAI.CriticalPercolation.BinaryLaw.fromWords_sides_marks line 26
  5. lemma OAI.CriticalPercolation.BinaryLaw.sides_fromWords line 34
  6. lemma OAI.CriticalPercolation.BinaryLaw.marks_fromWords line 40
  7. def OAI.CriticalPercolation.BinaryLaw.wordsEquiv line 46
  8. lemma OAI.CriticalPercolation.BinaryLaw.interval_fromWords line 52
  9. lemma OAI.CriticalPercolation.BinaryLaw.nextIndex_fromWords line 58
  10. lemma OAI.CriticalPercolation.BinaryLaw.anchors_fromWords line 62
  11. lemma OAI.CriticalPercolation.BinaryLaw.anchorSet_fromWords line 71
  12. def OAI.CriticalPercolation.BinaryLaw.historyPrefix line 76
  13. lemma OAI.CriticalPercolation.BinaryLaw.prefix_self line 81
  14. lemma OAI.CriticalPercolation.BinaryLaw.prefix_prev line 86
  15. lemma OAI.CriticalPercolation.BinaryLaw.prefix_last line 90
  16. lemma OAI.CriticalPercolation.BinaryLaw.prefix_fromWords line 93
  17. lemma OAI.CriticalPercolation.BinaryLaw.anchors_sides line 109
  18. lemma OAI.CriticalPercolation.BinaryLaw.interval_sides line 116
  19. lemma OAI.CriticalPercolation.BinaryLaw.nextIndex_sides line 123
  20. lemma OAI.CriticalPercolation.BinaryLaw.density_prefix_support line 132