OAI/Combinatorics/ContingencyTables/Sampling/UnitTrialProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

All-small trials and retries use only the stored profile entries

  1. def OAI.ContingencyTables.ProfilePrograms.unitPackedWords line 10
  2. def OAI.ContingencyTables.ProfilePrograms.unitPackedWordsRealizer line 12
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitPackedWords line 16
  4. def OAI.ContingencyTables.ProfilePrograms.unitPackedState line 21
  5. def OAI.ContingencyTables.ProfilePrograms.unitPackedStateRealizer line 23
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitPackedState line 27
  7. def OAI.ContingencyTables.ProfilePrograms.unitPackedTrial line 31
  8. def OAI.ContingencyTables.ProfilePrograms.unitPackedTrialRealizer line 33
  9. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitPackedTrial line 40
  10. def OAI.ContingencyTables.ProfilePrograms.unitRetryWidth line 45
  11. def OAI.ContingencyTables.ProfilePrograms.unitRetryWidthRealizer line 46
  12. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitRetryWidth line 52
  13. def OAI.ContingencyTables.ProfilePrograms.unitRetryWords line 60
  14. def OAI.ContingencyTables.ProfilePrograms.unitRetryWordsRealizer line 61
  15. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitRetryWords line 65
  16. def OAI.ContingencyTables.ProfilePrograms.unitProfileRetry line 68
  17. def OAI.ContingencyTables.ProfilePrograms.unitProfileRetryRealizer line 70
  18. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitProfileRetry line 75