OAI/Combinatorics/LowSpaceSubsetSum/Counting/SamplerExecution.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Counter-carrying execution of finite sampler compositions

The value fields agree with the bounded samplers. A dependent bind does not execute its second sampler after first-stage exhaustion. Counts are retained on every branch, including failure; ideal backup values do not add candidate reads to the bounded execution.

  1. structure OAI.LowSpaceSubsetSum.SamplerExecution.Trace line 23
  2. structure OAI.LowSpaceSubsetSum.SamplerExecution.Execution line 28
  3. theorem OAI.LowSpaceSubsetSum.SamplerExecution.Execution.ideal_eq_of_some line 32
  4. def OAI.LowSpaceSubsetSum.SamplerExecution.Execution.Bounded line 40
  5. theorem OAI.LowSpaceSubsetSum.SamplerExecution.Execution.Bounded.mono line 44
  6. def OAI.LowSpaceSubsetSum.SamplerExecution.cast line 49
  7. theorem OAI.LowSpaceSubsetSum.SamplerExecution.cast_bounded line 52
  8. def OAI.LowSpaceSubsetSum.SamplerExecution.pure line 60
  9. theorem OAI.LowSpaceSubsetSum.SamplerExecution.pure_bounded line 64
  10. def OAI.LowSpaceSubsetSum.SamplerExecution.map line 66
  11. theorem OAI.LowSpaceSubsetSum.SamplerExecution.map_bounded line 71
  12. def OAI.LowSpaceSubsetSum.SamplerExecution.bind line 74
  13. theorem OAI.LowSpaceSubsetSum.SamplerExecution.bind_run_some line 92

    Source documentation

    On acceptance, the dependent second stage is exactly the stage indexed by the value actually returned by the first stage. The cast changes only its type, so no ideal backup value is needed to choose a runtime branch.

    theorem bind_run_some {S : SamplerCoupling α} (X : Execution S)
    (B : α → Type) [∀ a, Fintype (B a)] (T : ∀ a, SamplerCoupling (B a))
    (Y : ∀ a, Execution (T a)) (s : S.Seed) (a : α)
    (h : (X.run s).value = some a) (t : (T (S.ideal s)).Seed) :
    let ha := X.ideal_eq_of_some s a h
…

    Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.SamplerExecution.Execution

  14. theorem OAI.LowSpaceSubsetSum.SamplerExecution.bind_bounded line 106
  15. def OAI.LowSpaceSubsetSum.SamplerExecution.prod line 119
  16. theorem OAI.LowSpaceSubsetSum.SamplerExecution.prod_bounded line 123
  17. def OAI.LowSpaceSubsetSum.SamplerExecution.pi line 129
  18. theorem OAI.LowSpaceSubsetSum.SamplerExecution.pi_bounded line 137
  19. def OAI.LowSpaceSubsetSum.SamplerExecution.certify line 156
  20. theorem OAI.LowSpaceSubsetSum.SamplerExecution.certify_firstAccept line 163
  21. def OAI.LowSpaceSubsetSum.SamplerExecution.test line 172
  22. theorem OAI.LowSpaceSubsetSum.SamplerExecution.test_bounded line 190
  23. def OAI.LowSpaceSubsetSum.SamplerExecution.range line 198
  24. theorem OAI.LowSpaceSubsetSum.SamplerExecution.range_bounded line 205
  25. def OAI.LowSpaceSubsetSum.SamplerExecution.prime line 216
  26. theorem OAI.LowSpaceSubsetSum.SamplerExecution.prime_bounded line 223
  27. def OAI.LowSpaceSubsetSum.SamplerExecution.fin line 234
  28. theorem OAI.LowSpaceSubsetSum.SamplerExecution.fin_bounded line 239
  29. def OAI.LowSpaceSubsetSum.SamplerExecution.permutation line 246
  30. theorem OAI.LowSpaceSubsetSum.SamplerExecution.permutation_bounded line 250
  31. def OAI.LowSpaceSubsetSum.SamplerExecution.finiteChoice line 260
  32. theorem OAI.LowSpaceSubsetSum.SamplerExecution.finiteChoice_bounded line 264
  33. def OAI.LowSpaceSubsetSum.SamplerExecution.finitePermutation line 267
  34. theorem OAI.LowSpaceSubsetSum.SamplerExecution.finitePermutation_bounded line 271
  35. def OAI.LowSpaceSubsetSum.SamplerExecution.coloring line 275
  36. theorem OAI.LowSpaceSubsetSum.SamplerExecution.coloring_bounded line 280