OAI/Combinatorics/ContingencyTables/Sampling/SmallProfileValidator.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary validator for the positive profile space

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileCheckData line 11
  2. def OAI.ContingencyTables.ProfilePrograms.profileViews line 13
  3. def OAI.ContingencyTables.ProfilePrograms.profileCatalog line 16
  4. def OAI.ContingencyTables.ProfilePrograms.profileMargins line 19
  5. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileViews line 22
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileCatalog line 25
  7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileMargins line 28
  8. def OAI.ContingencyTables.ProfilePrograms.profileView line 31
  9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileView line 35
  10. def OAI.ContingencyTables.ProfilePrograms.profileBound line 40
  11. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileBound line 44
  12. def OAI.ContingencyTables.ProfilePrograms.profileShape line 48
  13. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileShape line 53
  14. def OAI.ContingencyTables.ProfilePrograms.profilePattern line 58
  15. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profilePattern line 61
  16. def OAI.ContingencyTables.ProfilePrograms.profileColumnView line 65
  17. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileColumnView line 69
  18. def OAI.ContingencyTables.ProfilePrograms.profileLineData line 73
  19. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileLineData line 78
  20. def OAI.ContingencyTables.ProfilePrograms.profileLineTest line 83
  21. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileLineTest line 88
  22. def OAI.ContingencyTables.ProfilePrograms.profileTest line 91
  23. def OAI.ContingencyTables.ProfilePrograms.profileTestRealizer line 100
  24. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileTest line 109
  25. theorem OAI.ContingencyTables.SmallGraphProfiles.profileTest_iff line 129