OAI/Combinatorics/ContingencyTables/Machines/SparseViewMatrixProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Materializing a sparse retained-cell view in a rectangular matrix

  1. abbrev OAI.ContingencyTables.SparseViewMatrixProgram.Input line 14
  2. abbrev OAI.ContingencyTables.SparseViewMatrixProgram.RowInput line 15
  3. def OAI.ContingencyTables.SparseViewMatrixProgram.entry line 17
  4. def OAI.ContingencyTables.SparseViewMatrixProgram.entryRealizer line 18
  5. lemma OAI.ContingencyTables.SparseViewMatrixProgram.polynomial_entry line 22
  6. def OAI.ContingencyTables.SparseViewMatrixProgram.columns line 28
  7. def OAI.ContingencyTables.SparseViewMatrixProgram.columnsRealizer line 29
  8. lemma OAI.ContingencyTables.SparseViewMatrixProgram.polynomial_columns line 31
  9. def OAI.ContingencyTables.SparseViewMatrixProgram.row line 39
  10. def OAI.ContingencyTables.SparseViewMatrixProgram.rowRealizer line 40
  11. lemma OAI.ContingencyTables.SparseViewMatrixProgram.polynomial_row line 42
  12. def OAI.ContingencyTables.SparseViewMatrixProgram.rowIndices line 46
  13. def OAI.ContingencyTables.SparseViewMatrixProgram.rowIndicesRealizer line 47
  14. lemma OAI.ContingencyTables.SparseViewMatrixProgram.polynomial_rowIndices line 49
  15. def OAI.ContingencyTables.SparseViewMatrixProgram.matrix line 56
  16. def OAI.ContingencyTables.SparseViewMatrixProgram.matrixRealizer line 57
  17. theorem OAI.ContingencyTables.SparseViewMatrixProgram.polynomial_matrix line 59
  18. theorem OAI.ContingencyTables.SparseViewMatrixProgram.matrix_ofFn line 63