Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Sampling finite choices with a fixed supply of fair bits

Lax253009.FreshBitSampling · concepts/Lax253009/FreshBitSampling.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    To sample NN choices from r>0r>0 possibilities, use b=⌈log⁡2(12Nr)⌉b=\lceil\log_2(12Nr)\rceil independent bits per choice and reduce the binary integer modulo rr. This always returns a choice and uses exactly NbNb bits. Its effect on the probability of any event is at most 1/121/12. Thus the graph reduction's 1/41/4 error becomes at most 1/31/3, while perfect completeness is unchanged.

    The sampler uses explicit binary interpretation and natural-number remainder. The probability theorem does not certify its running time on the registered probabilistic Turing-machine model.

    Concept map
    2 concepts; 2 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 flat_one_third_error proven

    2 modulo_error proven

    3 one_third_error proven

    4 repeated_seed_bit_bound proven

    5 sampling_error proven

    Lean source view on GitHub

    1import Lax253009.FiniteProbability
    2import Mathlib.Algebra.BigOperators.Fin
    3import Mathlib.Data.Nat.Log
    4
    5/-!
    6---
    7title: Sampling finite choices with a fixed supply of fair bits
    8type: theorem
    9---
    10To sample NN choices from r>0r>0 possibilities, use
    11b=⌈log⁡2(12Nr)⌉b=\lceil\log_2(12Nr)\rceil independent bits per choice and reduce the
    12binary integer modulo rr. This always returns a choice and uses exactly
    13NbNb bits. Its effect on the probability of any event is at most 1/121/12.
    14Thus the graph reduction's 1/41/4 error becomes at most 1/31/3, while perfect
    15completeness is unchanged.
    16
    17The sampler uses explicit binary interpretation and natural-number
    18remainder. The probability theorem does not certify its running time on
    19the registered probabilistic Turing-machine model.
    20-/
    21
    22namespace Lax253009.FreshBitSampling
    23
    24open FiniteProbability
    25
    26def modulo {N r B : ℕ} (hr : 0 < r) (z : Fin N → Fin B) : Fin N → Fin r :=
    27 fun i ↦ ⟨(z i).val % r, Nat.mod_lt _ hr⟩
    28
    29def bitsPerDraw (N r : ℕ) : ℕ := Nat.clog 2 (12 * N * r)
    30
    31def binaryEquiv (b : ℕ) : (Fin b → Bool) ≃ Fin (2 ^ b) :=
    32 (Equiv.piCongrRight (fun _ ↦ finTwoEquiv.symm)).trans finFunctionFinEquiv
    33
    34def sample {N r : ℕ} (hr : 0 < r)
    35 (z : Fin N → Fin (bitsPerDraw N r) → Bool) : Fin N → Fin r :=
    36 modulo hr (fun i ↦ binaryEquiv (bitsPerDraw N r) (z i))
    37
    38def coinEquiv (N b : ℕ) : (Fin (N * b) → Bool) ≃ (Fin N → Fin b → Bool) :=
    39 (Equiv.arrowCongr finProdFinEquiv.symm (Equiv.refl Bool)).trans (Equiv.curry _ _ _)
    40
    41def sampleFlat {N r : ℕ} (hr : 0 < r)
    42 (coins : Fin (N * bitsPerDraw N r) → Bool) : Fin N → Fin r :=
    43 sample hr (coinEquiv N (bitsPerDraw N r) coins)
    44
    45axiom modulo_error {N r B : ℕ} (hr : 0 < r) (hB : 0 < B)
    46 (P : (Fin N → Fin r) → Prop) :
    47 probability (fun z : Fin N → Fin B ↦ P (modulo hr z)) ≤
    48 probability P + (N : ℝ) * r / B
    49
    50axiom sampling_error {N r : ℕ} (hN : 0 < N) (hr : 0 < r)
    51 (P : (Fin N → Fin r) → Prop) :
    52 probability (fun z : Fin N → Fin (bitsPerDraw N r) → Bool ↦ P (sample hr z)) ≤
    53 probability P + 1 / 12
    54
    55axiom one_third_error {N r : ℕ} (hN : 0 < N) (hr : 0 < r)
    56 (P : (Fin N → Fin r) → Prop) (hP : probability P ≤ 1 / 4) :
    57 probability (fun z : Fin N → Fin (bitsPerDraw N r) → Bool ↦ P (sample hr z)) ≤ 1 / 3
    58
    59axiom flat_one_third_error {N r : ℕ} (hN : 0 < N) (hr : 0 < r)
    60 (P : (Fin N → Fin r) → Prop) (hP : probability P ≤ 1 / 4) :
    61 probability (fun coins : Fin (N * bitsPerDraw N r) → Bool ↦ P (sampleFlat hr coins)) ≤ 1 / 3
    62
    63axiom repeated_seed_bit_bound (N r k : ℕ) :
    64 bitsPerDraw N (r ^ k) ≤ Nat.clog 2 (12 * N) + k * Nat.clog 2 r
    65
    66end Lax253009.FreshBitSampling
    67
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…