OAI/Combinatorics/ContingencyTables/Dense/DenseCompletedMatrixProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Binary construction of the completed integer matrix

  1. def OAI.ContingencyTables.DensePrograms.completedEntry line 10
  2. def OAI.ContingencyTables.DensePrograms.completedEntryRealizer line 12
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_completedEntry line 15
  4. def OAI.ContingencyTables.DensePrograms.completionRows line 19
  5. def OAI.ContingencyTables.DensePrograms.completionColumns line 20
  6. def OAI.ContingencyTables.DensePrograms.completionRowsRealizer line 22
  7. def OAI.ContingencyTables.DensePrograms.completionColumnsRealizer line 24
  8. lemma OAI.ContingencyTables.DensePrograms.polynomial_completionRows line 27
  9. lemma OAI.ContingencyTables.DensePrograms.polynomial_completionColumns line 34
  10. def OAI.ContingencyTables.DensePrograms.completedRowEntry line 41
  11. def OAI.ContingencyTables.DensePrograms.completedRowEntryRealizer line 42
  12. lemma OAI.ContingencyTables.DensePrograms.polynomial_completedRowEntry line 45
  13. def OAI.ContingencyTables.DensePrograms.completedRow line 50
  14. def OAI.ContingencyTables.DensePrograms.completedRowRealizer line 52
  15. lemma OAI.ContingencyTables.DensePrograms.polynomial_completedRow line 55
  16. def OAI.ContingencyTables.DensePrograms.completedMatrix line 60
  17. def OAI.ContingencyTables.DensePrograms.completedMatrixRealizer line 62
  18. theorem OAI.ContingencyTables.DensePrograms.polynomial_completedMatrix line 65
  19. lemma OAI.ContingencyTables.DensePrograms.completedEntry_code line 69
  20. lemma OAI.ContingencyTables.DensePrograms.optionIndex_finSucc line 79
  21. lemma OAI.ContingencyTables.DensePrograms.completedRow_code line 84
  22. theorem OAI.ContingencyTables.DensePrograms.completedMatrix_code line 101