OAI/Combinatorics/ContingencyTables/Sampling/ExactOrdinaryProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite ordinary branch of the exact sampler

  1. def OAI.ContingencyTables.ProfilePrograms.exactOrdinaryWord line 11
  2. def OAI.ContingencyTables.ProfilePrograms.exactOrdinaryWordRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_exactOrdinaryWord line 20
  4. def OAI.ContingencyTables.ProfilePrograms.exactOrdinary line 25
  5. def OAI.ContingencyTables.ProfilePrograms.exactOrdinaryRealizer line 28
  6. lemma OAI.ContingencyTables.ProfilePrograms.work_exactOrdinary line 31
  7. def OAI.ContingencyTables.ProfilePrograms.exactGate line 36

    Source documentation

    The gate retains the margins for either branch.

    def exactGate (z : CompletionMargins) : Experiment (Bool×CompletionMargins) :=
…
  8. def OAI.ContingencyTables.ProfilePrograms.exactGateRealizer line 39
  9. lemma OAI.ContingencyTables.ProfilePrograms.work_exactGate line 43
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.exactOrdinaryWord_code line 61