OAI/Combinatorics/ContingencyTables/Sampling/OriginalProfileProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Computing the initial profile directly from the greedy table

  1. abbrev OAI.ContingencyTables.ProfilePrograms.OriginalViewInput line 13
  2. def OAI.ContingencyTables.ProfilePrograms.originalFirstView line 15
  3. def OAI.ContingencyTables.ProfilePrograms.originalFirstViewRealizer line 17
  4. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_originalFirstView line 20
  5. def OAI.ContingencyTables.ProfilePrograms.originalViews line 24
  6. def OAI.ContingencyTables.ProfilePrograms.originalViewsRealizer line 26
  7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_originalViews line 30
  8. def OAI.ContingencyTables.ProfilePrograms.initialViewInput line 35
  9. def OAI.ContingencyTables.ProfilePrograms.initialViewInputRealizer line 37
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_initialViewInput line 40
  11. def OAI.ContingencyTables.ProfilePrograms.initialViews line 44
  12. def OAI.ContingencyTables.ProfilePrograms.initialViewsRealizer line 45
  13. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_initialViews line 47
  14. def OAI.ContingencyTables.ProfilePrograms.initialCheck line 50
  15. def OAI.ContingencyTables.ProfilePrograms.initialCheckRealizer line 51
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_initialCheck line 54
  17. lemma OAI.ContingencyTables.SmallGraphProfiles.originalViews_code line 67
  18. lemma OAI.ContingencyTables.SmallGraphProfiles.initialViews_code line 80
  19. lemma OAI.ContingencyTables.SmallGraphProfiles.initialCheck_code line 93