OAI/Combinatorics/ContingencyTables/Transport/DyadicAcceptance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-bit Metropolis acceptance

A uniform integer encoded by the allotted fair bits is compared with a power of two. Extra bits are padding; their number does not change the acceptance probability.

  1. abbrev OAI.ContingencyTables.FairBits.acceptDyadic line 17
  2. theorem OAI.ContingencyTables.FairBits.acceptDyadic_count line 20
  3. theorem OAI.ContingencyTables.FairBits.acceptDyadic_probability line 26
  4. theorem OAI.ContingencyTables.FairBits.dyadic_ratio_min line 37
  5. theorem OAI.ContingencyTables.GridBoundary.dense_acceptance_dyadic line 65