OAI/Combinatorics/ContingencyTables/Sampling/ExactBranchChoice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact dyadic gate that selects the rare correction branch

  1. def OAI.ContingencyTables.ProfilePrograms.rareWord line 12

    Source documentation

    All zero bits select correction; every other word selects the ordinary draw.

    def rareWord (z : CompletionMarginsĂ—List Bool) : Bool := decide (StackAddition.value z.2=0)
  2. def OAI.ContingencyTables.ProfilePrograms.rareWordRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_rareWord line 19
  4. def OAI.ContingencyTables.ProfilePrograms.rareBranch line 23
  5. def OAI.ContingencyTables.ProfilePrograms.rareBranchRealizer line 26
  6. lemma OAI.ContingencyTables.ProfilePrograms.work_rareBranch line 29
  7. lemma OAI.ContingencyTables.ProfilePrograms.rareBranch_probability line 36