OAI/Combinatorics/ContingencyTables/Dense/DenseTrialProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The complete dense trial as a polynomial binary program

  1. abbrev OAI.ContingencyTables.DensePrograms.DenseTrialData line 12
  2. def OAI.ContingencyTables.DensePrograms.fiftiethPower line 14
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_fiftiethPower line 20
  4. def OAI.ContingencyTables.DensePrograms.trialWalkBits line 24
  5. def OAI.ContingencyTables.DensePrograms.trialWalkBitsRealizer line 27
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_trialWalkBits line 37
  7. def OAI.ContingencyTables.DensePrograms.trialGrid line 50
  8. def OAI.ContingencyTables.DensePrograms.trialGridRealizer line 53
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_trialGrid line 62
  10. def OAI.ContingencyTables.DensePrograms.trialOffsets line 69
  11. def OAI.ContingencyTables.DensePrograms.trialOffsetsRealizer line 72
  12. theorem OAI.ContingencyTables.DensePrograms.polynomial_trialOffsets line 77
  13. def OAI.ContingencyTables.DensePrograms.trialCompletion line 84
  14. def OAI.ContingencyTables.DensePrograms.trialCompletionRealizer line 87
  15. theorem OAI.ContingencyTables.DensePrograms.polynomial_trialCompletion line 91
  16. def OAI.ContingencyTables.DensePrograms.acceptCompletion line 95
  17. def OAI.ContingencyTables.DensePrograms.acceptCompletionRealizer line 98
  18. theorem OAI.ContingencyTables.DensePrograms.polynomial_acceptCompletion line 101
  19. def OAI.ContingencyTables.DensePrograms.denseTrialCode line 105
  20. def OAI.ContingencyTables.DensePrograms.denseTrialCodeRealizer line 107
  21. theorem OAI.ContingencyTables.DensePrograms.polynomial_denseTrialCode line 112

    Source documentation

    Includes the full walk, every quotient offset, signed-entry checking, and binary output construction. Runtime is polynomial for every input.

    theorem polynomial_denseTrialCode : PolynomialTime denseTrialCodeRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.denseTrialCodeRealizer