OAI/Combinatorics/ContingencyTables/Dense/DenseDrawProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The bounded dense draw as a single polynomial binary program

  1. abbrev OAI.ContingencyTables.DensePrograms.DenseDrawParameters line 11
  2. abbrev OAI.ContingencyTables.DensePrograms.DenseDrawData line 12
  3. def OAI.ContingencyTables.DensePrograms.trialWidth line 14
  4. def OAI.ContingencyTables.DensePrograms.trialWidthRealizer line 17
  5. theorem OAI.ContingencyTables.DensePrograms.polynomial_trialWidth line 25
  6. def OAI.ContingencyTables.DensePrograms.drawChunks line 34
  7. def OAI.ContingencyTables.DensePrograms.drawChunksRealizer line 37
  8. theorem OAI.ContingencyTables.DensePrograms.polynomial_drawChunks line 41
  9. def OAI.ContingencyTables.DensePrograms.denseDrawCode line 46
  10. def OAI.ContingencyTables.DensePrograms.denseDrawCodeRealizer line 49
  11. theorem OAI.ContingencyTables.DensePrograms.polynomial_denseDrawCode line 54

    Source documentation

    Every finite input has polynomial binary cost. On a valid dense input, the first successful trial is selected, or the supplied feasible fallback.

    theorem polynomial_denseDrawCode : PolynomialTime denseDrawCodeRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.denseDrawCodeRealizer