OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseContinuation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Continuing an adaptive phase from its initialized profile

  1. abbrev OAI.ContingencyTables.CompanionPhaseContinuation.Configs line 14
  2. abbrev OAI.ContingencyTables.CompanionPhaseContinuation.Stored line 15
  3. def OAI.ContingencyTables.CompanionPhaseContinuation.state line 17
  4. def OAI.ContingencyTables.CompanionPhaseContinuation.width line 20
  5. def OAI.ContingencyTables.CompanionPhaseContinuation.input line 23
  6. def OAI.ContingencyTables.CompanionPhaseContinuation.run line 28
  7. lemma OAI.ContingencyTables.CompanionPhaseContinuation.outer_eq line 31
  8. lemma OAI.ContingencyTables.CompanionPhaseContinuation.view_getD line 38
  9. lemma OAI.ContingencyTables.CompanionPhaseContinuation.input_encoded line 45
  10. theorem OAI.ContingencyTables.CompanionPhaseContinuation.run_sameLaw line 69