OAI/Combinatorics/ContingencyTables/Sampling/ProfileScheduleProgram.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Computing the complete outer sampling schedule from binary margins

  1. abbrev OAI.ContingencyTables.ProfilePrograms.SamplingParameters line 13
  2. def OAI.ContingencyTables.ProfilePrograms.squarePower line 15
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_squarePower line 18
  4. def OAI.ContingencyTables.ProfilePrograms.cubicPower line 21
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_cubicPower line 25
  6. def OAI.ContingencyTables.ProfilePrograms.twelfthPower line 29
  7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_twelfthPower line 33
  8. def OAI.ContingencyTables.ProfilePrograms.twoHundredthPower line 36
  9. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_twoHundredthPower line 40
  10. def OAI.ContingencyTables.ProfilePrograms.sixtySecondPower line 43
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_sixtySecondPower line 47
  12. def OAI.ContingencyTables.ProfilePrograms.marginPadding line 52
  13. def OAI.ContingencyTables.ProfilePrograms.marginPaddingRealizer line 54
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginPadding line 57
  15. def OAI.ContingencyTables.ProfilePrograms.marginStateBound line 60
  16. def OAI.ContingencyTables.ProfilePrograms.marginStateBoundRealizer line 62
  17. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginStateBound line 65
  18. def OAI.ContingencyTables.ProfilePrograms.marginBinaryLength line 68
  19. def OAI.ContingencyTables.ProfilePrograms.marginBinaryLengthRealizer line 70
  20. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_marginBinaryLength line 73
  21. def OAI.ContingencyTables.ProfilePrograms.parameterDimension line 76
  22. def OAI.ContingencyTables.ProfilePrograms.parameterDimensionRealizer line 78
  23. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterDimension line 81
  24. def OAI.ContingencyTables.ProfilePrograms.parameterBinaryLength line 84
  25. def OAI.ContingencyTables.ProfilePrograms.parameterBinaryLengthRealizer line 86
  26. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterBinaryLength line 89
  27. def OAI.ContingencyTables.ProfilePrograms.parameterTrials line 92
  28. def OAI.ContingencyTables.ProfilePrograms.parameterTrialsRealizer line 94
  29. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterTrials line 97
  30. def OAI.ContingencyTables.ProfilePrograms.parameterSteps line 100
  31. def OAI.ContingencyTables.ProfilePrograms.parameterStepsRealizer line 102
  32. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterSteps line 105
  33. def OAI.ContingencyTables.ProfilePrograms.parameterAccuracy line 108
  34. def OAI.ContingencyTables.ProfilePrograms.parameterAccuracyRealizer line 110
  35. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterAccuracy line 113
  36. def OAI.ContingencyTables.ProfilePrograms.parameterProposalWidth line 116
  37. def OAI.ContingencyTables.ProfilePrograms.parameterProposalWidthRealizer line 118
  38. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterProposalWidth line 121
  39. def OAI.ContingencyTables.ProfilePrograms.parameterCompletionWidth line 124
  40. def OAI.ContingencyTables.ProfilePrograms.parameterCompletionWidthRealizer line 126
  41. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterCompletionWidth line 129
  42. def OAI.ContingencyTables.ProfilePrograms.parameterWordCount line 132
  43. def OAI.ContingencyTables.ProfilePrograms.parameterWordCountRealizer line 134
  44. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parameterWordCount line 137