OAI/Combinatorics/ContingencyTables/Machines/ScaledWordProgram.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary execution of the bounded quotient draw

  1. def OAI.ContingencyTables.ProfilePrograms.scaledWordValue line 11
  2. def OAI.ContingencyTables.ProfilePrograms.scaledWordRealizer line 14
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_scaledWord line 21
  4. theorem OAI.ContingencyTables.ProfilePrograms.scaledWordValue_ofFn line 28
  5. theorem OAI.ContingencyTables.ProfilePrograms.scaledWordValue_lt line 34

    Source documentation

    Every finite input yields the prescribed bounded integer.

    theorem scaledWordValue_lt (M : ℕ) (hM : 0<M) (bits : List Bool) :
    scaledWordValue (M,bits)<M := by
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.scaledWordValue