OAI/Combinatorics/ContingencyTables/Machines/DyadicWordProgram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary evaluation of the finite Metropolis coin

  1. def OAI.ContingencyTables.DensePrograms.dyadicWordAccept line 11
  2. def OAI.ContingencyTables.DensePrograms.dyadicWordAcceptRealizer line 16

    Source documentation

    The power of two is built from a prefix of the supplied word. Thus no binary integer supplied as a gap can cause an unbounded expansion.

    def dyadicWordAcceptRealizer : Realizer dyadicWordAccept := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.dyadicWordAccept

  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_dyadicWordAccept line 25
  4. theorem OAI.ContingencyTables.DensePrograms.dyadicWordAccept_ofFn line 37