OAI/Combinatorics/ContingencyTables/Transport/IntegerMatrixPoint.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Propagating an executable point mass through an integer matrix

  1. def OAI.ContingencyTables.IntegerMatrixPrograms.pointEntry line 10
  2. def OAI.ContingencyTables.IntegerMatrixPrograms.pointEntryRealizer line 12
  3. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_pointEntry line 18
  4. def OAI.ContingencyTables.IntegerMatrixPrograms.pointVector line 25
  5. def OAI.ContingencyTables.IntegerMatrixPrograms.pointVectorRealizer line 28
  6. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_pointVector line 32
  7. def OAI.ContingencyTables.IntegerMatrixPrograms.fromPoint line 41
  8. def OAI.ContingencyTables.IntegerMatrixPrograms.fromPointInputRealizer line 44
  9. def OAI.ContingencyTables.IntegerMatrixPrograms.fromPointRealizer line 48
  10. lemma OAI.ContingencyTables.IntegerMatrixPrograms.polynomial_fromPointInput line 51
  11. lemma OAI.ContingencyTables.IntegerMatrixPrograms.work_fromPoint line 56
  12. lemma OAI.ContingencyTables.IntegerMatrixPrograms.pointVector_ofFn line 76
  13. lemma OAI.ContingencyTables.IntegerMatrixPrograms.fromPoint_ofFn line 87