OAI/Combinatorics/ContingencyTables/Sampling/ExactPublicPrefix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The fixed exact-sampling machine on the literal public binary tape

  1. def OAI.ContingencyTables.ExactPublicPrefix.middle line 14

    Source documentation

    These two finite programs are independent of dimensions and margins.

    def middle : Program := ExactPhysicalProgram.program.seq LiteralProgram.post

    Mentions: OAI.ContingencyTables.LiteralProgram.post

  2. def OAI.ContingencyTables.ExactPublicPrefix.program line 15
  3. def OAI.ContingencyTables.ExactPublicPrefix.machine line 17
  4. def OAI.ContingencyTables.ExactPublicPrefix.word line 21
  5. lemma OAI.ContingencyTables.ExactPublicPrefix.word_eq line 23
  6. def OAI.ContingencyTables.ExactPublicPrefix.middleOutput line 26
  7. def OAI.ContingencyTables.ExactPublicPrefix.output line 30
  8. lemma OAI.ContingencyTables.ExactPublicPrefix.middle_prefix line 32
  9. theorem OAI.ContingencyTables.ExactPublicPrefix.prefix_correct line 67
  10. lemma OAI.ContingencyTables.ExactPublicPrefix.output_none_live line 90
  11. lemma OAI.ContingencyTables.ExactPublicPrefix.output_halted line 94
  12. lemma OAI.ContingencyTables.ExactPublicPrefix.output_tape line 96