OAI/Combinatorics/ContingencyTables/Sampling/ExactGatePublic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The cheap gate prefix on public binary input

  1. lemma OAI.ContingencyTables.ExactGatePublic.feasible line 19
  2. lemma OAI.ContingencyTables.ExactGatePublic.print_bound line 30
  3. def OAI.ContingencyTables.ExactGatePublic.experiment line 40
  4. lemma OAI.ContingencyTables.ExactGatePublic.failure line 43
  5. def OAI.ContingencyTables.ExactGatePublic.output line 54
  6. lemma OAI.ContingencyTables.ExactGatePublic.output_injective line 57
  7. theorem OAI.ContingencyTables.ExactGatePublic.table_prefix line 85
  8. def OAI.ContingencyTables.ExactGatePublic.budget line 106
  9. def OAI.ContingencyTables.ExactGatePublic.publicOutput line 109
  10. lemma OAI.ContingencyTables.ExactGatePublic.publicOutput_halted line 111
  11. theorem OAI.ContingencyTables.ExactGatePublic.prefix_correct_cost line 113