OAI/Combinatorics/ContingencyTables/Sampling/ProfileMatrixProgram.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.ProfilePrograms.MatrixColumnInput line 11
  2. abbrev OAI.ContingencyTables.ProfilePrograms.MatrixColumnEntryInput line 12
  3. def OAI.ContingencyTables.ProfilePrograms.columnEntryInput line 14
  4. def OAI.ContingencyTables.ProfilePrograms.columnEntryInputRealizer line 17
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_columnEntryInput line 20
  6. def OAI.ContingencyTables.ProfilePrograms.columnEntry line 24
  7. def OAI.ContingencyTables.ProfilePrograms.columnEntryRealizer line 26
  8. def OAI.ContingencyTables.ProfilePrograms.columnEntryMeasure line 29
  9. lemma OAI.ContingencyTables.ProfilePrograms.work_columnEntry line 32
  10. def OAI.ContingencyTables.ProfilePrograms.matrixColumn line 46
  11. def OAI.ContingencyTables.ProfilePrograms.matrixColumnRealizer line 49
  12. def OAI.ContingencyTables.ProfilePrograms.matrixColumnMeasure line 58
  13. lemma OAI.ContingencyTables.ProfilePrograms.work_matrixColumn line 62
  14. def OAI.ContingencyTables.ProfilePrograms.profileMatrix line 90
  15. def OAI.ContingencyTables.ProfilePrograms.profileMatrixRealizer line 93
  16. def OAI.ContingencyTables.ProfilePrograms.profileMatrixMeasure line 100
  17. lemma OAI.ContingencyTables.ProfilePrograms.work_profileMatrix line 104