OAI/Combinatorics/ContingencyTables/Counting/CountingDirectProgram.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

The direct estimator for the zero-label branch

The same finite-word median evaluator handles this branch. The confidence parameter controls the outer repetition count independently of its relative accuracy, which is one quarter of the public accuracy.

  1. abbrev OAI.ContingencyTables.CountingDirectProgram.Input line 16
  2. def OAI.ContingencyTables.CountingDirectProgram.accuracy line 18
  3. def OAI.ContingencyTables.CountingDirectProgram.accuracyRealizer line 19
  4. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_accuracy line 22
  5. def OAI.ContingencyTables.CountingDirectProgram.reserve line 27
  6. def OAI.ContingencyTables.CountingDirectProgram.reserveRealizer line 28
  7. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_reserve line 29
  8. def OAI.ContingencyTables.CountingDirectProgram.oracleInput line 32
  9. def OAI.ContingencyTables.CountingDirectProgram.oracleInputRealizer line 34
  10. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_oracleInput line 39
  11. def OAI.ContingencyTables.CountingDirectProgram.rawConfig line 46
  12. def OAI.ContingencyTables.CountingDirectProgram.rawConfigRealizer line 47
  13. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_rawConfig line 50
  14. def OAI.ContingencyTables.CountingDirectProgram.context line 54
  15. def OAI.ContingencyTables.CountingDirectProgram.contextRealizer line 55
  16. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_context line 56
  17. def OAI.ContingencyTables.CountingDirectProgram.repeats line 59
  18. def OAI.ContingencyTables.CountingDirectProgram.repeatsRealizer line 60
  19. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_repeats line 63
  20. def OAI.ContingencyTables.CountingDirectProgram.markers line 67
  21. def OAI.ContingencyTables.CountingDirectProgram.markersRealizer line 68
  22. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_markers line 69
  23. def OAI.ContingencyTables.CountingDirectProgram.config line 73
  24. def OAI.ContingencyTables.CountingDirectProgram.configRealizer line 74
  25. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_config line 75
  26. def OAI.ContingencyTables.CountingDirectProgram.contextWidth line 79
  27. def OAI.ContingencyTables.CountingDirectProgram.contextWidthRealizer line 80
  28. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_contextWidth line 83
  29. def OAI.ContingencyTables.CountingDirectProgram.wordWidth line 87
  30. def OAI.ContingencyTables.CountingDirectProgram.wordWidthRealizer line 88
  31. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_wordWidth line 92
  32. def OAI.ContingencyTables.CountingDirectProgram.sampleBits line 95
  33. def OAI.ContingencyTables.CountingDirectProgram.sampleBitsRealizer line 96
  34. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_sampleBits line 99
  35. def OAI.ContingencyTables.CountingDirectProgram.medianInput line 102
  36. def OAI.ContingencyTables.CountingDirectProgram.medianInputRealizer line 103
  37. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_medianInput line 105
  38. def OAI.ContingencyTables.CountingDirectProgram.output line 109
  39. def OAI.ContingencyTables.CountingDirectProgram.outputRealizer line 110
  40. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_output line 113
  41. abbrev OAI.ContingencyTables.CountingDirectProgram.Request line 117
  42. def OAI.ContingencyTables.CountingDirectProgram.empty line 119
  43. def OAI.ContingencyTables.CountingDirectProgram.emptyRealizer line 120
  44. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_empty line 121
  45. def OAI.ContingencyTables.CountingDirectProgram.padding line 123
  46. def OAI.ContingencyTables.CountingDirectProgram.paddingRealizer line 126
  47. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_padding line 131
  48. def OAI.ContingencyTables.CountingDirectProgram.budget line 138
  49. def OAI.ContingencyTables.CountingDirectProgram.budgetRealizer line 139
  50. lemma OAI.ContingencyTables.CountingDirectProgram.polynomial_budget line 141