OAI/Combinatorics/ContingencyTables/Sampling/SmallRepairCodeProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Forward and inverse repairs on the stored pair of integer lists

  1. abbrev OAI.ContingencyTables.ProfilePrograms.RepairData line 10
  2. abbrev OAI.ContingencyTables.ProfilePrograms.LabelledRepairData line 11
  3. def OAI.ContingencyTables.ProfilePrograms.repairDataCatalog line 13
  4. def OAI.ContingencyTables.ProfilePrograms.repairDataRows line 16
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_repairDataCatalog line 19
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_repairDataRows line 22
  7. def OAI.ContingencyTables.ProfilePrograms.repairDataCaps line 26
  8. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_repairDataCaps line 30
  9. def OAI.ContingencyTables.ProfilePrograms.repairDataCross line 35
  10. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_repairDataCross line 39
  11. def OAI.ContingencyTables.ProfilePrograms.forwardRepairCode line 43
  12. def OAI.ContingencyTables.ProfilePrograms.forwardRepairCodeRealizer line 47
  13. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_forwardRepairCode line 51
  14. def OAI.ContingencyTables.ProfilePrograms.inverseRepairCode line 57
  15. def OAI.ContingencyTables.ProfilePrograms.inverseRepairCodeRealizer line 61
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_inverseRepairCode line 66
  17. theorem OAI.ContingencyTables.SmallGraphProfiles.forwardRepairCode_eq line 82
  18. theorem OAI.ContingencyTables.SmallGraphProfiles.inverseRepairCode_eq line 101