bend-collections-laws-math

Search uses release 1.0.0.0 · 5,526 definitions

Releases (1)

def cm2the same count taken over the pairs 2y, 2y + 1 with y < N
def split
def pair_eq[2a == k] + [2a + 1 == k] == [a == k / 2]
def bit_dbl0
def half_dbl0
def bit_dbl1
def half_dbl1
def pair_andwith m = 2h + 1: the pair 2y, 2y + 1 draws k once exactly when y draws k / 2 one width lower with h
def pairsthe pairs one width up count what the lower width counts
def and0x & 0 == 0
def cm0n = 1: every output draws 0
def cm0k
def div_one
def div_double2a / 2n = a / n
def bitsq_bbit * bit == bit
def and_selfx & x is the low w bits of x
def dbl0
def decompm = bit(m) + 2 half(m)
def and_evenn = 2h + 2, m = 2h + 1: n & m is twice (h + 1) & h one width lower
def and_oddn = 2g + 3, m = 2g + 2: n & m is twice the low bits of g + 1
def maskTHEOREM (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
def draw_maskthe draw is the mask when n is a power of two
def count_mask
def unbiased_c
def unbiasedTHEOREM (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

def eqm_of
def v
def carry_value
def fTthe cross products mod 2^64
def fSa sum mod 2^64
def fVadding the carry
def step_pairone step for any product pair (l, h) with l + 2^64 h == lo * ml (the pair is abstract here, so the checker never unfolds the 128-bit product)
def m128

def low_l
def low_r
def low_addcongruence mod 2^k is kept by sums
def low_low
def low_himod 2^128, a + 2^64 b depends on b mod 2^64 = lb only
def perm7(((a + c) + d) + (e + g)) + (b + f) == (a + b) + (((c + (e + d)) + f) + g)
def swap3(L + x) + (y + z) == L + ((y + x) + z)
def shx2^64 ((((h + (p2 + p1)) + i) + c) + 2^64 p3), distributed
def expands * M + I == L + 2^64 Z for Z = ((((h + (P2 + P1)) + i) + c) + 2^64 P3)
def eqm_of
def high_wordthe new high word is Z mod 2^64 (t, vH, u: the sums of the implementation)
def step_valueTHEOREM on values: the limb results are the LCG step mod 2^128 (the state s, multiplier mul and increment inc given by their limbs)

def PCG.step
def PCG.constants
def v
def xsx ^ (x >> k)
def plus1
def or_valuelo | 1
def mulgthe value of a product mod 2^64 from the values of its factors; the factors stay variables here, so no product is ever normalized
def xs32
def xs48
def xtx ^ (x >> 48) for a word of value t
def half1the first half's value is t
def PCG.outputTHEOREM (PCG.output) values are known (x ^ x >> 48 with x of value t, and lo | 1)

def occ
def some_or
def is_some
def none_some
def some_inj
def swap_ends(a + c) + b == (b + c) + a
def assoc3(h + x) + y == h + (x + y), stated for the step of put_occ
def put_occwriting x over the element y at i: occ + [y] == old occ + [x]
def nth_putwriting y at i keeps an element y at j
def swap_some
def swap_m_occ
def swap_occTHEOREM: a swap keeps every count
def swap_at_occ
def go_occ
def shuffle_permTHEOREM (Shuffle.permutation)
def lt_succ_split[p == v] + [v < p] == [v < p + 1]
def range_occrange_go(n, acc) = [0, 1, ..., n - 1] ++ acc holds v as often as acc, plus once when v < n
def perm_permTHEOREM (Perm.permutation)