OAI/Combinatorics/ContingencyTables/Dense/DenseMatrixLayoutProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Polynomial conversion between flat and rectangular grid encodings

  1. abbrev OAI.ContingencyTables.DensePrograms.GridFlatData line 11
  2. def OAI.ContingencyTables.DensePrograms.sliceRow line 13
  3. def OAI.ContingencyTables.DensePrograms.sliceRowRealizer line 16
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_sliceRow line 22
  5. def OAI.ContingencyTables.DensePrograms.layoutRows line 31
  6. def OAI.ContingencyTables.DensePrograms.layoutRowsRealizer line 33
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_layoutRows line 36
  8. def OAI.ContingencyTables.DensePrograms.layoutRow line 45
  9. def OAI.ContingencyTables.DensePrograms.layoutRowRealizer line 48
  10. theorem OAI.ContingencyTables.DensePrograms.polynomial_layoutRow line 53
  11. def OAI.ContingencyTables.DensePrograms.unflattenGrid line 60
  12. def OAI.ContingencyTables.DensePrograms.unflattenGridRealizer line 63
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_unflattenGrid line 66
  14. lemma OAI.ContingencyTables.DensePrograms.flatten_matrixCode line 70
  15. lemma OAI.ContingencyTables.DensePrograms.sliceRow_ofFn line 83
  16. theorem OAI.ContingencyTables.DensePrograms.unflattenGrid_code line 99