OAI/Combinatorics/ContingencyTables/Machines/RepeatedFractionProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Independent repetition of a finite-word rational program

The public confidence amplification only groups bits already supplied on the tape. Its binary count cannot cause an unbounded allocation.

  1. abbrev OAI.ContingencyTables.RepeatedFractionProgram.Input line 17
  2. def OAI.ContingencyTables.RepeatedFractionProgram.words line 19
  3. def OAI.ContingencyTables.RepeatedFractionProgram.wordsRealizer line 21
  4. lemma OAI.ContingencyTables.RepeatedFractionProgram.polynomial_words line 28
  5. def OAI.ContingencyTables.RepeatedFractionProgram.sample line 38
  6. def OAI.ContingencyTables.RepeatedFractionProgram.sampleRealizer line 40
  7. lemma OAI.ContingencyTables.RepeatedFractionProgram.polynomial_sample line 43
  8. def OAI.ContingencyTables.RepeatedFractionProgram.samples line 49
  9. def OAI.ContingencyTables.RepeatedFractionProgram.samplesRealizer line 51
  10. lemma OAI.ContingencyTables.RepeatedFractionProgram.polynomial_samples line 53
  11. def OAI.ContingencyTables.RepeatedFractionProgram.output line 60
  12. def OAI.ContingencyTables.RepeatedFractionProgram.outputRealizer line 62
  13. lemma OAI.ContingencyTables.RepeatedFractionProgram.polynomial_output line 65
  14. theorem OAI.ContingencyTables.RepeatedFractionProgram.output_ofFn line 72