OAI/Combinatorics/LowSpaceSubsetSum/Word/WordProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Sequential fair-word programs for the bounded samplers

A draw reads one fresh word. Continuations are evaluated only after that word is read. The finite expectation is the operational probability law; there are no eligible-backup draws in this interface.

  1. inductive OAI.LowSpaceSubsetSum.WordProgram.Program line 17
  2. def OAI.LowSpaceSubsetSum.WordProgram.bind line 23
  3. def OAI.LowSpaceSubsetSum.WordProgram.map line 27
  4. def OAI.LowSpaceSubsetSum.WordProgram.expectation line 29
  5. def OAI.LowSpaceSubsetSum.WordProgram.probability line 33
  6. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_bind line 36
  7. theorem OAI.LowSpaceSubsetSum.WordProgram.probability_map line 43
  8. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_sum line 47
  9. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_mul line 55
  10. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_eq_sum line 63
  11. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_of_probability line 74
  12. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_const line 80
  13. theorem OAI.LowSpaceSubsetSum.WordProgram.probability_true line 89
  14. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_nonneg line 93
  15. theorem OAI.LowSpaceSubsetSum.WordProgram.expectation_mono line 100
  16. def OAI.LowSpaceSubsetSum.WordProgram.run line 108

    Source documentation

    A read-only random stream supplies the words in order.

    def run (stream : ℕ → Fin (2^w)) : Program w α → ℕ → α × ℕ
  | .pure a, offset => (a, offset)
  | .draw next, offset => run stream (next (stream offset)) (offset+1)

/-- A structural draw bound, independent of the stream's values. -/

    Mentions: OAI.LowSpaceSubsetSum.WordProgram.Program

  17. inductive OAI.LowSpaceSubsetSum.WordProgram.Bounded line 113

    Source documentation

    A structural draw bound, independent of the stream's values.

    inductive Bounded : Program w α → ℕ → Prop where
…

    Mentions: OAI.LowSpaceSubsetSum.WordProgram.Program

  18. theorem OAI.LowSpaceSubsetSum.WordProgram.run_bound line 118
  19. theorem OAI.LowSpaceSubsetSum.WordProgram.bound_add line 129
  20. theorem OAI.LowSpaceSubsetSum.WordProgram.bind_bound line 136