OAI/Combinatorics/ContingencyTables/Sampling/ProfileRetryProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A polynomial retry loop for the complete binary outer trial

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileRetryParameters line 11
  2. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileRetryData line 12
  3. def OAI.ContingencyTables.ProfilePrograms.profileTrialWidth line 14
  4. def OAI.ContingencyTables.ProfilePrograms.profileRetryWordInput line 17
  5. def OAI.ContingencyTables.ProfilePrograms.profileRetryWordInputRealizer line 18
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileRetryWordInput line 21
  7. def OAI.ContingencyTables.ProfilePrograms.profileTrialWidthRealizer line 25
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileTrialWidth line 29
  9. def OAI.ContingencyTables.ProfilePrograms.profileRetryWords line 36
  10. def OAI.ContingencyTables.ProfilePrograms.profileRetryWordsRealizer line 38
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileRetryWords line 41
  12. def OAI.ContingencyTables.ProfilePrograms.profileRetry line 45
  13. def OAI.ContingencyTables.ProfilePrograms.profileRetryRealizer line 47
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileRetry line 51