OAI/Combinatorics/LowSpaceSubsetSum/Storage/SamplerVectorCells.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Stored candidate tuples for certified bounded samplers

The runtime argument is a vector of candidate words. Its function view is used only to identify the finite sampling law. Certification and the unused ideal backup do not perform another candidate search.

  1. def OAI.LowSpaceSubsetSum.SamplerVectorCells.candidates line 17
  2. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.raw_value line 20
  3. def OAI.LowSpaceSubsetSum.SamplerVectorCells.test line 26
  4. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.test_value line 39
  5. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.test_cells line 49
  6. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.test_seed_independent line 58
  7. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.rangeNonempty line 70
  8. def OAI.LowSpaceSubsetSum.SamplerVectorCells.range line 73
  9. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.range_value line 80
  10. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.range_cells line 89
  11. def OAI.LowSpaceSubsetSum.SamplerVectorCells.rangeSeed line 100

    Source documentation

    Tabulate the supplied finite random-word tuple once. The extra reserve counts both tabulation storage and its construction stack.

    def rangeSeed (s : (rangeCoupling hD n).Seed) : SamplerExecution.Trace (Fin D) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.rangeCoupling, OAI.LowSpaceSubsetSum.SamplerExecution.Trace

  12. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.rangeSeed_value line 105
  13. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.rangeSeed_cells line 114
  14. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.primeNonempty line 127
  15. def OAI.LowSpaceSubsetSum.SamplerVectorCells.prime line 131
  16. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.prime_value line 139
  17. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.prime_cells line 150
  18. def OAI.LowSpaceSubsetSum.SamplerVectorCells.primeSeed line 160
  19. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.primeSeed_value line 166
  20. theorem OAI.LowSpaceSubsetSum.SamplerVectorCells.primeSeed_cells line 175