OAI/Combinatorics/ContingencyTables/Machines/RetryNumeratorProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Binary first-success numerators via a two-coordinate recurrence

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

    Source documentation

    Unary trial count; denominator, failure count, success count, fallback match.

    abbrev Input := List Bool×((ℕ×ℕ)×(ℕ×Bool))
  2. def OAI.ContingencyTables.RetryNumeratorPrograms.twoEntries line 14
  3. lemma OAI.ContingencyTables.RetryNumeratorPrograms.polynomial_twoEntries line 17
  4. def OAI.ContingencyTables.RetryNumeratorPrograms.setup line 22
  5. def OAI.ContingencyTables.RetryNumeratorPrograms.setupRealizer line 25
  6. lemma OAI.ContingencyTables.RetryNumeratorPrograms.polynomial_setup line 37
  7. def OAI.ContingencyTables.RetryNumeratorPrograms.count line 56
  8. def OAI.ContingencyTables.RetryNumeratorPrograms.countRealizer line 58
  9. theorem OAI.ContingencyTables.RetryNumeratorPrograms.polynomial_count line 63

    Source documentation

    All stored numbers are binary; only the supplied trial marker controls iteration, so evaluation is polynomial in that marker and binary data.

    theorem polynomial_count : PolynomialTime countRealizer := by
…

    Mentions: OAI.ContingencyTables.RetryNumeratorPrograms.countRealizer

  10. def OAI.ContingencyTables.RetryNumeratorPrograms.recurrence line 75
  11. lemma OAI.ContingencyTables.RetryNumeratorPrograms.iterate_eq line 79
  12. lemma OAI.ContingencyTables.RetryNumeratorPrograms.propagate_two line 87
  13. lemma OAI.ContingencyTables.RetryNumeratorPrograms.count_eq line 93
  14. lemma OAI.ContingencyTables.RetryNumeratorPrograms.recurrence_retry line 109