proofs/math/random/lemire.bend checks

lo < n and lo < t is lo < t, when t < n

the hit of an accepted or rejected hi

s <= t + s

hi < k: rejected or not, x n lies below both thresholds

hi == k: x n is below the upper threshold, and below the lower one exactly when it is rejected

hi > k: x n is at or above both thresholds

THEOREM (one output, Lemire's branch): with t = 2^w mod n < n and k 2^w + t <= (k + 1) 2^w, y = x n draws k exactly when k 2^w + t <= y < (k + 1) 2^w

#{x < N : x n < c}

the draw is Lemire's when n is not a power of two

(a + h) + (b + e) == (a + b) + (h + e)

the Lemire outputs below N plus those with x n below the lower threshold are those with x n below the upper one

a + 1 <= b is a < b

x n < c is x < ceil(c / n) = (c + n - 1) / n, n = 1 + bp

min(N + 1, C) = min(N, C) + [N < C]

THEOREM: #{x < N : x n < c} = min(N, ceil(c / n))

Go's -n % n: 2^w mod n

(q n + r) / n = q + r / n

a <= b and c < d give a + c < b + d

ceil((k + 1) 2^w / n) <= 2^w for k < n

t <= 2^w for t < n <= 2^w

(k + 1) 2^w + m = q n + (t + k 2^w + m), q n + t = 2^w

THEOREM (Lemire's branch): floor(2^w / n) outputs draw k

#{x < N : and_bits(w, x, m) == k}

the same count taken over the pairs 2y, 2y + 1 with y < N

[2a == k] + [2a + 1 == k] == [a == k / 2]

with m = 2h + 1: the pair 2y, 2y + 1 draws k once exactly when y draws k / 2 one width lower with h

the pairs one width up count what the lower width counts

x & 0 == 0

n = 1: every output draws 0

2a / 2n = a / n

bit * bit == bit

x & x is the low w bits of x

m = bit(m) + 2 half(m)

n = 2h + 2, m = 2h + 1: n & m is twice (h + 1) & h one width lower

n = 2g + 3, m = 2g + 2: n & m is twice the low bits of g + 1

THEOREM (the mask branch): with n = 1 + m, n & m == 0 and n < 2^v, each k < n is the low bits of floor(2^v / n) outputs

the draw is the mask when n is a power of two

THEOREM (Lemire.unbiased): for every width w, bound 0 < n < 2^w and k < n, exactly floor(2^w / n) of the 2^w outputs draw k