OAI/Combinatorics/ContingencyTables/Counting/CountingExecutedMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

One fixed counting machine with the computed adaptive program

  1. abbrev OAI.ContingencyTables.CountingExecutedMachine.positive line 13
  2. abbrev OAI.ContingencyTables.CountingExecutedMachine.positiveWidth line 14
  3. def OAI.ContingencyTables.CountingExecutedMachine.positiveRealizer line 16
  4. def OAI.ContingencyTables.CountingExecutedMachine.positiveWidthRealizer line 20
  5. lemma OAI.ContingencyTables.CountingExecutedMachine.polynomial_positive line 23
  6. lemma OAI.ContingencyTables.CountingExecutedMachine.polynomial_positiveWidth line 29
  7. def OAI.ContingencyTables.CountingExecutedMachine.machine line 33
  8. def OAI.ContingencyTables.CountingExecutedMachine.machineTime line 36
  9. abbrev OAI.ContingencyTables.CountingExecutedMachine.wordCount line 39
  10. abbrev OAI.ContingencyTables.CountingExecutedMachine.publicOutput line 40
  11. abbrev OAI.ContingencyTables.CountingExecutedMachine.sourceValue line 41
  12. theorem OAI.ContingencyTables.CountingExecutedMachine.public_time line 43
  13. theorem OAI.ContingencyTables.CountingExecutedMachine.outputs_nonnegative line 58
  14. theorem OAI.ContingencyTables.CountingExecutedMachine.outputs_zero line 66