OAI/Combinatorics/LowSpaceSubsetSum/Counting/BoundedSampling.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Bounded rejection sampling

The executable sampler reads at most the supplied number of candidates. All probability statements use the uniform law on the finite candidate tuples, which is exactly independent sampling with replacement.

  1. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_eq_cardRatio line 21
  2. def OAI.LowSpaceSubsetSum.firstAccept line 27

    Source documentation

    Read candidates in their given order and return the first eligible value.

    def firstAccept (A : Ω → Prop) [DecidablePred A] :
    (N : ℕ) → (Fin N → Ω) → Option Ω
  | 0, _ => none
  | N + 1, f => if A (f 0) then some (f 0)
      else firstAccept A N (fun i => f i.succ)
  3. theorem OAI.LowSpaceSubsetSum.firstAccept_eq_none_iff line 33
  4. theorem OAI.LowSpaceSubsetSum.firstAccept_some_eligible line 43
  5. theorem OAI.LowSpaceSubsetSum.firstAccept_failure line 53
  6. def OAI.LowSpaceSubsetSum.firstAcceptCount line 63
  7. def OAI.LowSpaceSubsetSum.firstAcceptFiberSuccEquiv line 68
  8. theorem OAI.LowSpaceSubsetSum.firstAcceptCount_succ line 104
  9. theorem OAI.LowSpaceSubsetSum.firstAcceptCount_conservation line 113
  10. theorem OAI.LowSpaceSubsetSum.firstAccept_value_probability line 134

    Source documentation

    The exact subprobability of every eligible return value.

    theorem firstAccept_value_probability [Fintype Ω] [Nonempty Ω]
    (A : Ω → Prop) [DecidablePred A] (N : ℕ) (a : Ω) (ha : A a) :
    finiteUniformProbability (fun f : Fin N → Ω => firstAccept A N f = some a) =
      (1 - (1 - finiteUniformProbability A) ^ N) / Fintype.card {b : Ω // A b} := by
…

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.firstAccept

  11. theorem OAI.LowSpaceSubsetSum.firstAccept_acceptance line 156
  12. theorem OAI.LowSpaceSubsetSum.firstAccept_conditional_uniform line 163

    Source documentation

    Conditioning only this call on acceptance gives the uniform eligible law.

    theorem firstAccept_conditional_uniform [Fintype Ω] [Nonempty Ω]
    (A : Ω → Prop) [DecidablePred A] (N : ℕ) (hN : 0 < N) (a : Ω) (ha : A a) :
    finiteUniformProbability (fun f : Fin N → Ω => firstAccept A N f = some a) /
        finiteUniformProbability (fun f : Fin N → Ω => firstAccept A N f ≠ none) =
      1 / Fintype.card {b : Ω // A b} := by
…

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.firstAccept

  13. theorem OAI.LowSpaceSubsetSum.firstAccept_failure_le_exp line 180
  14. theorem OAI.LowSpaceSubsetSum.card_fin_lt line 195
  15. def OAI.LowSpaceSubsetSum.rangeEligible line 205

    Source documentation

    Rejection predicate for the clog₂ D fresh low bits.

    def rangeEligible (D : ℕ) (x : Fin (2 ^ Nat.clog 2 D)) : Prop := x.val < D
  16. instance OAI.LowSpaceSubsetSum.(instance at line 207) line 207
  17. theorem OAI.LowSpaceSubsetSum.rangeEligible_probability line 209
  18. theorem OAI.LowSpaceSubsetSum.rangeEligible_probability_lower line 223
  19. theorem OAI.LowSpaceSubsetSum.rangeSampler_failure line 236
  20. def OAI.LowSpaceSubsetSum.primeEligible line 247

    Source documentation

    Exactly the prime test performed on an ell-bit candidate.

    def primeEligible (ell : ℕ) (x : Fin (2 ^ ell)) : Prop := x.val ∈ primeRange ell

    Mentions: OAI.LowSpaceSubsetSum.primeRange

  21. instance OAI.LowSpaceSubsetSum.(instance at line 249) line 249
  22. theorem OAI.LowSpaceSubsetSum.primeEligible_probability line 251
  23. theorem OAI.LowSpaceSubsetSum.primeEligible_probability_lower line 263
  24. theorem OAI.LowSpaceSubsetSum.primeSampler_failure line 272
  25. def OAI.LowSpaceSubsetSum.completedFirstAccept line 288

    Source documentation

    Complete an exhausted bounded call with an independent eligible backup. This is the ideal marginal in the explicit one-call coupling.

    def completedFirstAccept (A : Ω → Prop) [DecidablePred A] (N : ℕ)
    (f : Fin N → Ω) (backup : {a : Ω // A a}) : Ω :=
…
  26. theorem OAI.LowSpaceSubsetSum.completedFirstAccept_eligible line 292
  27. theorem OAI.LowSpaceSubsetSum.completedFirstAccept_mismatch_iff line 298
  28. def OAI.LowSpaceSubsetSum.firstAcceptNoneEquiv line 304
  29. theorem OAI.LowSpaceSubsetSum.firstAccept_none_card line 312
  30. def OAI.LowSpaceSubsetSum.completedFirstAcceptFiberEquiv line 319
  31. theorem OAI.LowSpaceSubsetSum.completedFirstAccept_uniform line 360

    Source documentation

    The ideal marginal is exactly uniform; the backup introduces no bias.

    theorem completedFirstAccept_uniform [Fintype Ω] [Nonempty Ω]
    (A : Ω → Prop) [DecidablePred A] (N : ℕ) (a : Ω) (ha : A a) :
    finiteUniformProbability
      (fun z : (Fin N → Ω) × {b : Ω // A b} => completedFirstAccept A N z.1 z.2 = a) =
        1 / Fintype.card {b : Ω // A b} := by
…

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.completedFirstAccept

  32. theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_fst line 386
  33. theorem OAI.LowSpaceSubsetSum.firstAccept_coupling_mismatch line 407

    Source documentation

    In the explicit finite coupling, disagreement is exactly exhaustion of the bounded call. The first marginal is the original independent candidate tuple.

    theorem firstAccept_coupling_mismatch [Fintype Ω] [Nonempty Ω]
    (A : Ω → Prop) [DecidablePred A] [Nonempty {a : Ω // A a}] (N : ℕ) :
    finiteUniformProbability
      (fun z : (Fin N → Ω) × {a : Ω // A a} =>
        some (completedFirstAccept A N z.1 z.2) ≠ firstAccept A N z.1) =
      (1 - finiteUniformProbability A) ^ N := by
…

    Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.completedFirstAccept, OAI.LowSpaceSubsetSum.firstAccept