OAI/Combinatorics/ContingencyTables/Machines/NaturalBlockProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Bounded scans of natural-number blocks

Numeric widths select bounded slices of the supplied list. They never control an allocation, so malformed widths preserve polynomial cost.

  1. abbrev OAI.ContingencyTables.NaturalBlockProgram.Input line 16
  2. abbrev OAI.ContingencyTables.NaturalBlockProgram.Entry line 17
  3. def OAI.ContingencyTables.NaturalBlockProgram.start line 19
  4. def OAI.ContingencyTables.NaturalBlockProgram.startRealizer line 20
  5. lemma OAI.ContingencyTables.NaturalBlockProgram.polynomial_start line 22
  6. def OAI.ContingencyTables.NaturalBlockProgram.block line 27
  7. def OAI.ContingencyTables.NaturalBlockProgram.blockRealizer line 29
  8. lemma OAI.ContingencyTables.NaturalBlockProgram.polynomial_block line 33
  9. def OAI.ContingencyTables.NaturalBlockProgram.indices line 42
  10. def OAI.ContingencyTables.NaturalBlockProgram.indicesRealizer line 43
  11. lemma OAI.ContingencyTables.NaturalBlockProgram.polynomial_indices line 44
  12. def OAI.ContingencyTables.NaturalBlockProgram.blocks line 50
  13. def OAI.ContingencyTables.NaturalBlockProgram.blocksRealizer line 51
  14. theorem OAI.ContingencyTables.NaturalBlockProgram.polynomial_blocks line 53
  15. lemma OAI.ContingencyTables.NaturalBlockProgram.block_splitLengths line 57
  16. theorem OAI.ContingencyTables.NaturalBlockProgram.blocks_eq_splitLengths line 68
  17. lemma OAI.ContingencyTables.NaturalBlockProgram.splitLengths_flatten line 79
  18. theorem OAI.ContingencyTables.NaturalBlockProgram.blocks_flatten line 89

    Source documentation

    A literal list of rows is recovered exactly from its stored row lengths and its flattened code, including rows of length zero.

    theorem blocks_flatten (rows : List (List ℕ)) :
    blocks (rows.map List.length,rows.flatten)=rows := by
…

    Mentions: OAI.ContingencyTables.NaturalBlockProgram.blocks