OAI/Combinatorics/ContingencyTables/Dense/DenseIntegerProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Binary list arithmetic for integral dense completion

  1. abbrev OAI.ContingencyTables.DensePrograms.MatrixCode line 13
  2. def OAI.ContingencyTables.DensePrograms.columnRead line 15
  3. def OAI.ContingencyTables.DensePrograms.columnReadRealizer line 17
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_columnRead line 20
  5. def OAI.ContingencyTables.DensePrograms.columnTotal line 23
  6. def OAI.ContingencyTables.DensePrograms.columnTotalRealizer line 25
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_columnTotal line 28
  8. def OAI.ContingencyTables.DensePrograms.rowTotal line 33
  9. def OAI.ContingencyTables.DensePrograms.rowTotalRealizer line 35
  10. theorem OAI.ContingencyTables.DensePrograms.polynomial_rowTotal line 37
  11. def OAI.ContingencyTables.DensePrograms.matrixTotal line 40
  12. def OAI.ContingencyTables.DensePrograms.matrixTotalRealizer line 42
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_matrixTotal line 44
  14. def OAI.ContingencyTables.DensePrograms.matrixEntry line 47
  15. def OAI.ContingencyTables.DensePrograms.matrixEntryRealizer line 49
  16. theorem OAI.ContingencyTables.DensePrograms.polynomial_matrixEntry line 53
  17. def OAI.ContingencyTables.DensePrograms.matrixCode line 59
  18. lemma OAI.ContingencyTables.DensePrograms.matrixEntry_code line 62
  19. lemma OAI.ContingencyTables.DensePrograms.rowTotal_code line 67
  20. lemma OAI.ContingencyTables.DensePrograms.columnTotal_code line 72
  21. lemma OAI.ContingencyTables.DensePrograms.matrixTotal_code line 77