OAI/Combinatorics/ContingencyTables/Machines/BooleanChunkProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial partition of a supplied Boolean word into fixed-width rows

  1. def OAI.ContingencyTables.DensePrograms.wordChunk line 10
  2. def OAI.ContingencyTables.DensePrograms.wordChunkRealizer line 13
  3. theorem OAI.ContingencyTables.DensePrograms.polynomial_wordChunk line 19
  4. def OAI.ContingencyTables.DensePrograms.completeWordRows line 28
  5. def OAI.ContingencyTables.DensePrograms.completeWordRowsRealizer line 30
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_completeWordRows line 33
  7. def OAI.ContingencyTables.DensePrograms.wordChunks line 42
  8. def OAI.ContingencyTables.DensePrograms.wordChunksRealizer line 45
  9. theorem OAI.ContingencyTables.DensePrograms.polynomial_wordChunks line 48
  10. lemma OAI.ContingencyTables.DensePrograms.wordChunk_ofFn line 52
  11. theorem OAI.ContingencyTables.DensePrograms.wordChunks_ofFn line 68