OAI/Combinatorics/LowSpaceSubsetSum/Storage/PermutationArray.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Materializing the finite permutation sampler's choices

The sampler's recursive finite-range choices are stored as integer digits. The construction below executes the same decomposeFin permutation using arrays, so applying the resulting permutation is a bounded array lookup.

  1. abbrev OAI.LowSpaceSubsetSum.PermutationArray.Digits line 14
  2. def OAI.LowSpaceSubsetSum.PermutationArray.semantic line 18
  3. def OAI.LowSpaceSubsetSum.PermutationArray.grow line 22
  4. def OAI.LowSpaceSubsetSum.PermutationArray.build line 26
  5. theorem OAI.LowSpaceSubsetSum.PermutationArray.grow_value line 32
  6. theorem OAI.LowSpaceSubsetSum.PermutationArray.build_value line 41
  7. theorem OAI.LowSpaceSubsetSum.PermutationArray.build_work line 49
  8. def OAI.LowSpaceSubsetSum.PermutationArray.lookup line 59
  9. theorem OAI.LowSpaceSubsetSum.PermutationArray.lookup_value line 61
  10. def OAI.LowSpaceSubsetSum.PermutationArray.peakCells line 66

    Source documentation

    The old and new arrays may coexist during one extension, together with the recursive digit stack. All are linear in the ambient input length.

    def peakCells : ℕ → ℕ
  | 0 => 3
  | k + 1 => max (peakCells k + 2) (3 * (k + 1) + 5)
  11. theorem OAI.LowSpaceSubsetSum.PermutationArray.peakCells_bound line 70