OAI/Combinatorics/ContingencyTables/Machines/VectorRetryProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

First-success propagation of an entire vector of integer counts

  1. abbrev OAI.ContingencyTables.VectorRetryPrograms.Input line 12

    Source documentation

    Trial marker, denominator, success counts, fallback index.

    abbrev Input := (List Bool×ℕ)×(List ℕ×ℕ)
  2. def OAI.ContingencyTables.VectorRetryPrograms.failure line 14
  3. def OAI.ContingencyTables.VectorRetryPrograms.failureRealizer line 16
  4. lemma OAI.ContingencyTables.VectorRetryPrograms.polynomial_failure line 20
  5. def OAI.ContingencyTables.VectorRetryPrograms.entryInput line 26
  6. def OAI.ContingencyTables.VectorRetryPrograms.entryInputRealizer line 29
  7. lemma OAI.ContingencyTables.VectorRetryPrograms.polynomial_entryInput line 40
  8. def OAI.ContingencyTables.VectorRetryPrograms.indices line 54
  9. def OAI.ContingencyTables.VectorRetryPrograms.indicesRealizer line 56
  10. lemma OAI.ContingencyTables.VectorRetryPrograms.polynomial_indices line 59
  11. def OAI.ContingencyTables.VectorRetryPrograms.counts line 66
  12. def OAI.ContingencyTables.VectorRetryPrograms.countsRealizer line 69
  13. theorem OAI.ContingencyTables.VectorRetryPrograms.polynomial_counts line 75

    Source documentation

    Binary vector propagation uses time polynomial in the success-vector encoding and in the supplied number of trial markers.

    theorem polynomial_counts : PolynomialTime countsRealizer :=
…

    Mentions: OAI.ContingencyTables.VectorRetryPrograms.countsRealizer

  14. lemma OAI.ContingencyTables.VectorRetryPrograms.failure_ofFn line 80
  15. theorem OAI.ContingencyTables.VectorRetryPrograms.counts_actual line 88