OAI/Combinatorics/LowSpaceSubsetSum/Counting/ExactWordDraw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact power-of-two draws from fair machine words

These projections discard high bits, so their law is exactly uniform. The rejection sampler's independent eligible backup is absent from the bounded execution and can be integrated out without changing its law.

  1. def OAI.LowSpaceSubsetSum.ExactWordDraw.low line 15
  2. def OAI.LowSpaceSubsetSum.ExactWordDraw.wordSplit line 18
  3. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.wordSplit_low line 23
  4. def OAI.LowSpaceSubsetSum.ExactWordDraw.tupleSplit line 28
  5. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.uniform_tuple line 42
  6. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.uniform_projection line 55
  7. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.firstAccept_no_backup line 62
  8. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.firstAccept_words line 73
  9. theorem OAI.LowSpaceSubsetSum.ExactWordDraw.candidates_words line 84

    Source documentation

    Full candidate observations may include the test and read counters.

    theorem candidates_words (w k : ℕ) (hk : k ≤ w)
    (A : Fin (2^k) → Prop) [DecidablePred A] [Nonempty {a : Fin (2^k) // A a}]
    (N : ℕ) (P : (Fin N → Fin (2^k)) → Prop) :
    (firstAcceptCoupling A N).law.probability (fun s => P s.1) =
      (FiniteLaw.uniform : FiniteLaw (Fin N → Fin (2^w))).probability
        (fun f => P (fun i => low w k (f i))) := by
…

    Mentions: OAI.LowSpaceSubsetSum.firstAcceptCoupling, OAI.LowSpaceSubsetSum.FiniteLaw.uniform, OAI.LowSpaceSubsetSum.FiniteLaw, OAI.LowSpaceSubsetSum.ExactWordDraw.low