OAI/Combinatorics/ContingencyTables/Machines/DependentWordProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Splitting a binary word at input-dependent coordinate widths

  1. abbrev OAI.ContingencyTables.DensePrograms.DependentChunkData line 11
  2. def OAI.ContingencyTables.DensePrograms.chunkStart line 13
  3. def OAI.ContingencyTables.DensePrograms.chunkStartRealizer line 14
  4. theorem OAI.ContingencyTables.DensePrograms.polynomial_chunkStart line 17
  5. def OAI.ContingencyTables.DensePrograms.dependentChunk line 22
  6. def OAI.ContingencyTables.DensePrograms.dependentChunkRealizer line 25
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_dependentChunk line 30
  8. def OAI.ContingencyTables.DensePrograms.chunkIndices line 39
  9. def OAI.ContingencyTables.DensePrograms.chunkIndicesRealizer line 40
  10. theorem OAI.ContingencyTables.DensePrograms.polynomial_chunkIndices line 42
  11. def OAI.ContingencyTables.DensePrograms.dependentChunks line 48
  12. def OAI.ContingencyTables.DensePrograms.dependentChunksRealizer line 50
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_dependentChunks line 53
  14. lemma OAI.ContingencyTables.DensePrograms.take_ofFn_sum line 59
  15. theorem OAI.ContingencyTables.DensePrograms.dependentChunk_ofFn line 64
  16. theorem OAI.ContingencyTables.DensePrograms.dependentChunks_ofFn line 89