OAI/Combinatorics/ContingencyTables/Machines/CompletionEnumerationProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Explicit free-box enumeration with binary completion tests

  1. abbrev OAI.ContingencyTables.DensePrograms.CompletionMargins line 13
  2. def OAI.ContingencyTables.DensePrograms.completionEnumerationData line 15
  3. def OAI.ContingencyTables.DensePrograms.completionEnumerationDataRealizer line 18
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_completionEnumerationData line 24
  5. def OAI.ContingencyTables.DensePrograms.completionCandidate line 31
  6. def OAI.ContingencyTables.DensePrograms.completionCandidateRealizer line 34
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_completionCandidate line 37
  8. def OAI.ContingencyTables.DensePrograms.completionCandidates line 43

    Source documentation

    Rejected candidates remain as none, allowing later integer sums to ignore them without adding a second enumeration or an ordering oracle.

    def completionCandidates (z : CompletionMargins) : List (Option MatrixCode) :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.CompletionMargins, OAI.ContingencyTables.DensePrograms.MatrixCode

  9. def OAI.ContingencyTables.DensePrograms.completionCandidatesRealizer line 46
  10. def OAI.ContingencyTables.DensePrograms.completionEnumerationMeasure line 50
  11. theorem OAI.ContingencyTables.DensePrograms.work_completionCandidates line 53
  12. lemma OAI.ContingencyTables.DensePrograms.gridWords_finFunctions line 75
  13. theorem OAI.ContingencyTables.DensePrograms.completionCandidates_code line 81