OAI/Combinatorics/ContingencyTables/Sampling/UnitMatrixProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Constructing the finite transition matrix by deterministic enumeration

  1. abbrev OAI.ContingencyTables.UnitCountPrograms.MatrixColumnInput line 10
  2. abbrev OAI.ContingencyTables.UnitCountPrograms.MatrixColumnEntryInput line 11
  3. def OAI.ContingencyTables.UnitCountPrograms.columnEntryInput line 13
  4. def OAI.ContingencyTables.UnitCountPrograms.columnEntryInputRealizer line 16
  5. lemma OAI.ContingencyTables.UnitCountPrograms.polynomial_columnEntryInput line 19
  6. def OAI.ContingencyTables.UnitCountPrograms.columnEntry line 23
  7. def OAI.ContingencyTables.UnitCountPrograms.columnEntryRealizer line 25
  8. def OAI.ContingencyTables.UnitCountPrograms.columnEntryMeasure line 28
  9. lemma OAI.ContingencyTables.UnitCountPrograms.work_columnEntry line 31
  10. def OAI.ContingencyTables.UnitCountPrograms.matrixColumn line 45
  11. def OAI.ContingencyTables.UnitCountPrograms.matrixColumnRealizer line 48
  12. def OAI.ContingencyTables.UnitCountPrograms.matrixColumnMeasure line 57
  13. lemma OAI.ContingencyTables.UnitCountPrograms.work_matrixColumn line 61
  14. def OAI.ContingencyTables.UnitCountPrograms.profileMatrix line 89
  15. def OAI.ContingencyTables.UnitCountPrograms.profileMatrixRealizer line 92
  16. def OAI.ContingencyTables.UnitCountPrograms.profileMatrixMeasure line 99
  17. lemma OAI.ContingencyTables.UnitCountPrograms.work_profileMatrix line 103