OAI/Combinatorics/ContingencyTables/Counting/CountingAdaptiveInputProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Original-input preparation for a positive-label counting run

  1. abbrev OAI.ContingencyTables.CountingAdaptiveInputProgram.Input line 13
  2. abbrev OAI.ContingencyTables.CountingAdaptiveInputProgram.Prepared line 14
  3. abbrev OAI.ContingencyTables.CountingAdaptiveInputProgram.Stored line 15
  4. abbrev OAI.ContingencyTables.CountingAdaptiveInputProgram.Output line 16
  5. def OAI.ContingencyTables.CountingAdaptiveInputProgram.prepared line 18
  6. def OAI.ContingencyTables.CountingAdaptiveInputProgram.preparedRealizer line 19
  7. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_prepared line 21
  8. def OAI.ContingencyTables.CountingAdaptiveInputProgram.capacities line 24
  9. def OAI.ContingencyTables.CountingAdaptiveInputProgram.capacitiesRealizer line 25
  10. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_capacities line 28
  11. def OAI.ContingencyTables.CountingAdaptiveInputProgram.labelWidth line 31
  12. def OAI.ContingencyTables.CountingAdaptiveInputProgram.labelWidthRealizer line 32
  13. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_labelWidth line 37
  14. def OAI.ContingencyTables.CountingAdaptiveInputProgram.zeroCode line 41
  15. def OAI.ContingencyTables.CountingAdaptiveInputProgram.zeroCodeRealizer line 42
  16. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_zeroCode line 47
  17. def OAI.ContingencyTables.CountingAdaptiveInputProgram.initialInput line 51
  18. def OAI.ContingencyTables.CountingAdaptiveInputProgram.initialInputRealizer line 53
  19. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_initialInput line 56
  20. def OAI.ContingencyTables.CountingAdaptiveInputProgram.initial line 60
  21. def OAI.ContingencyTables.CountingAdaptiveInputProgram.initialRealizer line 61
  22. lemma OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_initial line 64
  23. def OAI.ContingencyTables.CountingAdaptiveInputProgram.output line 67
  24. def OAI.ContingencyTables.CountingAdaptiveInputProgram.outputRealizer line 68
  25. theorem OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_output line 69
  26. def OAI.ContingencyTables.CountingAdaptiveInputProgram.runInput line 73

    Source documentation

    The outer confidence parameter is handled by independent repetition.

    def runInput (z : CountingDirectProgram.Input) : Output×List Bool := (output (z.1.1,z.2),z.2)

    Mentions: OAI.ContingencyTables.CountingDirectProgram.Input, OAI.ContingencyTables.CountingAdaptiveInputProgram.Output, OAI.ContingencyTables.CountingAdaptiveInputProgram.output

  27. def OAI.ContingencyTables.CountingAdaptiveInputProgram.runInputRealizer line 74
  28. theorem OAI.ContingencyTables.CountingAdaptiveInputProgram.polynomial_runInput line 77