OAI/Combinatorics/ContingencyTables/Sampling/OuterTableProgram.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Reconstructing and testing an original table from an outer trial

  1. abbrev OAI.ContingencyTables.ProfilePrograms.OuterTableData line 10
  2. abbrev OAI.ContingencyTables.ProfilePrograms.OuterTableCell line 12
  3. def OAI.ContingencyTables.ProfilePrograms.outputCellPosition line 14
  4. def OAI.ContingencyTables.ProfilePrograms.outputCellPositionRealizer line 15
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputCellPosition line 19
  6. def OAI.ContingencyTables.ProfilePrograms.outputSmallEntry line 25
  7. def OAI.ContingencyTables.ProfilePrograms.outputSmallEntryRealizer line 26
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputSmallEntry line 30
  9. def OAI.ContingencyTables.ProfilePrograms.outputDensePosition line 36
  10. def OAI.ContingencyTables.ProfilePrograms.outputDensePositionRealizer line 38
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputDensePosition line 44
  12. def OAI.ContingencyTables.ProfilePrograms.outputLargeEntry line 55
  13. def OAI.ContingencyTables.ProfilePrograms.outputLargeEntryRealizer line 57
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputLargeEntry line 62
  15. def OAI.ContingencyTables.ProfilePrograms.outputEntry line 71
  16. def OAI.ContingencyTables.ProfilePrograms.outputEntryRealizer line 73
  17. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputEntry line 79
  18. def OAI.ContingencyTables.ProfilePrograms.paddingTest line 87
  19. def OAI.ContingencyTables.ProfilePrograms.paddingTestRealizer line 88
  20. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_paddingTest line 92
  21. def OAI.ContingencyTables.ProfilePrograms.outerSuccess line 97
  22. def OAI.ContingencyTables.ProfilePrograms.outerSuccessRealizer line 100
  23. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outerSuccess line 107
  24. abbrev OAI.ContingencyTables.ProfilePrograms.OuterMatrixInput line 117
  25. def OAI.ContingencyTables.ProfilePrograms.outputShape line 119
  26. def OAI.ContingencyTables.ProfilePrograms.outputShapeRealizer line 120
  27. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputShape line 122
  28. def OAI.ContingencyTables.ProfilePrograms.outputRows line 125
  29. def OAI.ContingencyTables.ProfilePrograms.outputColumns line 126
  30. def OAI.ContingencyTables.ProfilePrograms.outputRowsRealizer line 127
  31. def OAI.ContingencyTables.ProfilePrograms.outputColumnsRealizer line 128
  32. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputRows line 130
  33. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputColumns line 132
  34. def OAI.ContingencyTables.ProfilePrograms.outputRowEntry line 135
  35. def OAI.ContingencyTables.ProfilePrograms.outputRowEntryRealizer line 136
  36. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputRowEntry line 140
  37. def OAI.ContingencyTables.ProfilePrograms.outputRow line 146
  38. def OAI.ContingencyTables.ProfilePrograms.outputRowRealizer line 148
  39. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputRow line 151
  40. def OAI.ContingencyTables.ProfilePrograms.outputMatrix line 156
  41. def OAI.ContingencyTables.ProfilePrograms.outputMatrixRealizer line 158
  42. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_outputMatrix line 161
  43. def OAI.ContingencyTables.ProfilePrograms.acceptedTable line 165
  44. def OAI.ContingencyTables.ProfilePrograms.acceptedTableRealizer line 167
  45. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_acceptedTable line 171