OAI/Combinatorics/ContingencyTables/Dense/DenseBooleanWalkProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A polynomial program for the complete flat-word dense walk

  1. def OAI.ContingencyTables.DensePrograms.denseWidthRealizer line 11
  2. theorem OAI.ContingencyTables.DensePrograms.polynomial_denseWidth line 16
  3. def OAI.ContingencyTables.DensePrograms.flatWordWalk line 25
  4. def OAI.ContingencyTables.DensePrograms.flatWordWalkRealizer line 28
  5. theorem OAI.ContingencyTables.DensePrograms.polynomial_flatWordWalk line 33
  6. lemma OAI.ContingencyTables.DensePrograms.denseStepBits_pos line 38
  7. theorem OAI.ContingencyTables.DensePrograms.flatWordWalk_code line 47

    Source documentation

    The literal flat-bit program computes exactly the finite Boolean walk. The polynomial runtime theorem above applies to every input word.

    theorem flatWordWalk_code {m n d : ℕ} (hd : 0<d)
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (a : Grid (I := Fin (m*n)) (4*d^8)) (steps : ℕ)
…