OAI/Combinatorics/ContingencyTables/Counting/CountingBranchProgram.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Public dispatch for the two counting branches

The positive-label evaluator is a program parameter, instantiated by the adaptive estimator. Feasibility and the zero-label branch are computed from the same parsed input used by the complete public machine.

  1. abbrev OAI.ContingencyTables.CountingBranchProgram.Request line 16
  2. abbrev OAI.ContingencyTables.CountingBranchProgram.Input line 17
  3. def OAI.ContingencyTables.CountingBranchProgram.request line 20

    Source documentation

    Reassociate the two rational parameters without re-encoding them.

    def request (z : CountingInputParser.Input) : Request := ((z.1,z.2.1),z.2.2)

    Mentions: OAI.ContingencyTables.CountingInputParser.Input, OAI.ContingencyTables.CountingBranchProgram.Request

  4. def OAI.ContingencyTables.CountingBranchProgram.requestRealizer line 21
  5. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_request line 23
  6. def OAI.ContingencyTables.CountingBranchProgram.feasible line 28
  7. def OAI.ContingencyTables.CountingBranchProgram.feasibleRealizer line 29
  8. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_feasible line 32
  9. def OAI.ContingencyTables.CountingBranchProgram.direct line 36
  10. def OAI.ContingencyTables.CountingBranchProgram.directRealizer line 37
  11. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_direct line 42
  12. def OAI.ContingencyTables.CountingBranchProgram.feasibleOutput line 52
  13. def OAI.ContingencyTables.CountingBranchProgram.feasibleOutputRealizer line 54
  14. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_feasibleOutput line 56
  15. def OAI.ContingencyTables.CountingBranchProgram.output line 63
  16. def OAI.ContingencyTables.CountingBranchProgram.outputRealizer line 65
  17. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_output line 67
  18. def OAI.ContingencyTables.CountingBranchProgram.parsedInput line 73
  19. def OAI.ContingencyTables.CountingBranchProgram.parsedInputRealizer line 75
  20. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_parsedInput line 77
  21. def OAI.ContingencyTables.CountingBranchProgram.publicOutput line 82
  22. def OAI.ContingencyTables.CountingBranchProgram.publicOutputRealizer line 84
  23. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_publicOutput line 88
  24. lemma OAI.ContingencyTables.CountingBranchProgram.publicOutput_eq line 93
  25. lemma OAI.ContingencyTables.CountingBranchProgram.publicOutput_symbols line 97
  26. lemma OAI.ContingencyTables.CountingBranchProgram.output_nonnegative line 101
  27. def OAI.ContingencyTables.CountingBranchProgram.feasibleBudget line 109
  28. def OAI.ContingencyTables.CountingBranchProgram.feasibleBudgetRealizer line 110
  29. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_feasibleBudget line 112
  30. def OAI.ContingencyTables.CountingBranchProgram.budget line 118
  31. def OAI.ContingencyTables.CountingBranchProgram.budgetRealizer line 119
  32. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_budget line 121
  33. def OAI.ContingencyTables.CountingBranchProgram.publicBudget line 126
  34. def OAI.ContingencyTables.CountingBranchProgram.publicBudgetRealizer line 127
  35. lemma OAI.ContingencyTables.CountingBranchProgram.polynomial_publicBudget line 130