OAI/Combinatorics/ContingencyTables/Sampling/OuterTrialProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Preparing the original-table return from a residual draw

  1. abbrev OAI.ContingencyTables.ProfilePrograms.OuterTrialInput line 10
  2. def OAI.ContingencyTables.ProfilePrograms.outputLargeRows line 12
  3. def OAI.ContingencyTables.ProfilePrograms.outputLargeColumns line 13
  4. def OAI.ContingencyTables.ProfilePrograms.outputLargeRowsRealizer line 15
  5. def OAI.ContingencyTables.ProfilePrograms.outputLargeColumnsRealizer line 19
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputLargeRows line 24
  7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputLargeColumns line 30
  8. def OAI.ContingencyTables.ProfilePrograms.outputData line 37
  9. def OAI.ContingencyTables.ProfilePrograms.outputDataRealizer line 39
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputData line 44
  11. def OAI.ContingencyTables.ProfilePrograms.prepareOutput line 53
  12. def OAI.ContingencyTables.ProfilePrograms.prepareOutputRealizer line 54
  13. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_prepareOutput line 57
  14. def OAI.ContingencyTables.ProfilePrograms.outerTrial line 62
  15. def OAI.ContingencyTables.ProfilePrograms.outerTrialRealizer line 63
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outerTrial line 66