OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseHistory.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual adaptive phases on a common finite Boolean word space

  1. structure OAI.ContingencyTables.RootedPhaseHistory.Settings line 23
  2. def OAI.ContingencyTables.RootedPhaseHistory.width line 37
  3. def OAI.ContingencyTables.RootedPhaseHistory.totalWidth line 42
  4. abbrev OAI.ContingencyTables.RootedPhaseHistory.Word line 45
  5. def OAI.ContingencyTables.RootedPhaseHistory.split line 47
  6. lemma OAI.ContingencyTables.RootedPhaseHistory.value_le_sum line 53
  7. lemma OAI.ContingencyTables.RootedPhaseHistory.width_le line 57
  8. def OAI.ContingencyTables.RootedPhaseHistory.step line 62
  9. def OAI.ContingencyTables.RootedPhaseHistory.decoded line 72
  10. lemma OAI.ContingencyTables.RootedPhaseHistory.decoded_nil line 76
  11. lemma OAI.ContingencyTables.RootedPhaseHistory.decoded_snoc line 79
  12. lemma OAI.ContingencyTables.RootedPhaseHistory.fold_length line 85
  13. lemma OAI.ContingencyTables.RootedPhaseHistory.decoded_length line 93
  14. lemma OAI.ContingencyTables.RootedPhaseHistory.good_snoc_iff line 97