OAI/Combinatorics/ContingencyTables/Sampling/SmallInverseRepairList.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Checking inverse repair candidates against their forward image

  1. def OAI.ContingencyTables.ProfilePrograms.inverseLabelInput line 11
  2. def OAI.ContingencyTables.ProfilePrograms.inverseLabelInputRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_inverseLabelInput line 18
  4. def OAI.ContingencyTables.ProfilePrograms.inverseLabelTest line 23
  5. def OAI.ContingencyTables.ProfilePrograms.inverseLabelTestRealizer line 27
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_inverseLabelTest line 33
  7. def OAI.ContingencyTables.ProfilePrograms.inverseRepairLabels line 41
  8. def OAI.ContingencyTables.ProfilePrograms.inverseRepairLabelsRealizer line 44
  9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_inverseRepairLabels line 47
  10. def OAI.ContingencyTables.ProfilePrograms.checkedInverseRepairList line 51
  11. def OAI.ContingencyTables.ProfilePrograms.checkedInverseRepairListRealizer line 54
  12. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_checkedInverseRepairList line 57
  13. theorem OAI.ContingencyTables.ProfilePrograms.checkedInverseRepairList_length line 61
  14. theorem OAI.ContingencyTables.SmallGraphProfiles.mem_checkedInverseRepairList line 76