OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationInitializationCells.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Live cells of shared-array row tournament initialization

  1. def OAI.LowSpaceSubsetSum.RepresentationInitializationCells.index line 14
  2. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.index_value line 20
  3. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.index_cells line 25
  4. def OAI.LowSpaceSubsetSum.RepresentationInitializationCells.front line 30
  5. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.front_value line 44
  6. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.front_cells line 53
  7. def OAI.LowSpaceSubsetSum.RepresentationInitializationCells.tree line 71
  8. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.tree_value line 79
  9. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.scale line 99
  10. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.padded_pow line 118
  11. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.tree_cells_raw line 123
  12. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.tree_cells line 138
  13. def OAI.LowSpaceSubsetSum.RepresentationInitializationCells.start line 151
  14. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.start_value line 169
  15. theorem OAI.LowSpaceSubsetSum.RepresentationInitializationCells.start_cells line 180