OAI/Combinatorics/ContingencyTables/Machines/FirstSuccessProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial first-success selection for a supplied list of trial words

  1. def OAI.ContingencyTables.FirstSuccessProgram.firstSome line 13
  2. def OAI.ContingencyTables.FirstSuccessProgram.isSomeRealizer line 18
  3. theorem OAI.ContingencyTables.FirstSuccessProgram.polynomial_isSome line 22
  4. lemma OAI.ContingencyTables.FirstSuccessProgram.firstSome_filter line 29
  5. def OAI.ContingencyTables.FirstSuccessProgram.firstSomeRealizer line 38
  6. theorem OAI.ContingencyTables.FirstSuccessProgram.polynomial_firstSome line 41
  7. def OAI.ContingencyTables.FirstSuccessProgram.defaultRealizer line 44
  8. theorem OAI.ContingencyTables.FirstSuccessProgram.polynomial_default line 48
  9. def OAI.ContingencyTables.FirstSuccessProgram.retry line 53
  10. def OAI.ContingencyTables.FirstSuccessProgram.retryRealizer line 56
  11. theorem OAI.ContingencyTables.FirstSuccessProgram.polynomial_retry line 62
  12. theorem OAI.ContingencyTables.FirstSuccessProgram.retry_ofFn line 75
  13. theorem OAI.ContingencyTables.FirstSuccessProgram.wordRetry_map line 89