OAI/Combinatorics/LowSpaceSubsetSum/Word/WordTuple.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite tuples drawn by sequential fair-word reads

  1. def OAI.LowSpaceSubsetSum.WordTuple.sample line 16
  2. theorem OAI.LowSpaceSubsetSum.WordTuple.bounded line 20
  3. theorem OAI.LowSpaceSubsetSum.WordTuple.uniform_product line 30
  4. theorem OAI.LowSpaceSubsetSum.WordTuple.product_expectation line 39
  5. theorem OAI.LowSpaceSubsetSum.WordTuple.uniform_word_expectation line 45
  6. theorem OAI.LowSpaceSubsetSum.WordTuple.cons_expectation line 51
  7. theorem OAI.LowSpaceSubsetSum.WordTuple.expectation line 60
  8. theorem OAI.LowSpaceSubsetSum.WordTuple.probability line 74