OAI/Combinatorics/ContingencyTables/Sampling/OriginalTableBox.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The full original-table box and its unique feasible entries

  1. abbrev OAI.ContingencyTables.OriginalTableBox.Box line 12
  2. abbrev OAI.ContingencyTables.OriginalTableBox.Index line 13
  3. def OAI.ContingencyTables.OriginalTableBox.matrix line 15
  4. def OAI.ContingencyTables.OriginalTableBox.decode line 18
  5. def OAI.ContingencyTables.OriginalTableBox.encode line 22
  6. lemma OAI.ContingencyTables.OriginalTableBox.matrix_encode line 27
  7. lemma OAI.ContingencyTables.OriginalTableBox.decode_encode line 32
  8. lemma OAI.ContingencyTables.OriginalTableBox.decode_eq_some line 39
  9. def OAI.ContingencyTables.OriginalTableBox.index line 56
  10. def OAI.ContingencyTables.OriginalTableBox.tableAt line 59
  11. lemma OAI.ContingencyTables.OriginalTableBox.tableAt_eq_some line 62
  12. lemma OAI.ContingencyTables.OriginalTableBox.freeMatrix_code line 73
  13. lemma OAI.ContingencyTables.OriginalTableBox.candidate_code line 79
  14. lemma OAI.ContingencyTables.OriginalTableBox.candidates_code line 91