OAI/Combinatorics/ContingencyTables/Dense/DenseSwapProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Binary row and column permutations for dense input normalization

  1. def OAI.ContingencyTables.DensePrograms.swapZeroIndex line 11
  2. def OAI.ContingencyTables.DensePrograms.swapZeroIndexRealizer line 13
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapZeroIndex line 18
  4. def OAI.ContingencyTables.DensePrograms.swapZeroEntry line 27
  5. def OAI.ContingencyTables.DensePrograms.swapZeroEntryRealizer line 30
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapZeroEntry line 34
  7. def OAI.ContingencyTables.DensePrograms.swapZeroIndices line 39
  8. def OAI.ContingencyTables.DensePrograms.swapZeroIndicesRealizer line 40
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapZeroIndices line 44
  10. def OAI.ContingencyTables.DensePrograms.swapZeroList line 49
  11. def OAI.ContingencyTables.DensePrograms.swapZeroListRealizer line 52
  12. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapZeroList line 55
  13. def OAI.ContingencyTables.DensePrograms.swapMatrixColumns line 59
  14. def OAI.ContingencyTables.DensePrograms.swapMatrixColumnsRealizer line 62
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapMatrixColumns line 64
  16. def OAI.ContingencyTables.DensePrograms.swapMatrix line 67
  17. def OAI.ContingencyTables.DensePrograms.swapMatrixRealizer line 70
  18. theorem OAI.ContingencyTables.DensePrograms.polynomial_swapMatrix line 74
  19. lemma OAI.ContingencyTables.DensePrograms.swapZeroIndex_val line 81
  20. theorem OAI.ContingencyTables.DensePrograms.swapZeroList_ofFn line 97
  21. theorem OAI.ContingencyTables.DensePrograms.swapMatrix_code line 110