Finite greedy allocation with uniform independent choices

Trace. For natural numbers $n,d$, a trace is an ordered array with $n+1$ rows and $d+2$ entries per row, each entry belonging to $\{0,\ldots,n\}$. Repeated entries within and between rows are permitted.

step. Given natural numbers $n,d$, a load function from $\{0,\ldots,n\}$ to the natural numbers, and an ordered list of $d+2$ choices in $\{0,\ldots,n\}$, select a choice having the smallest current load, breaking ties by the earliest occurrence in the list. Increase that selected bin’s load by one and leave all other loads unchanged.

finalLoads. For natural numbers $n,d$ and a trace with $n+1$ rows of $d+2$ bin choices each, start all $n+1$ bin loads at zero and process the rows in order. At each row, increase by one the load of the earliest minimum-load choice in that row. The result is the load function after exactly $n+1$ increments.

maxLoad. For natural numbers $n,d$ and a trace, take the largest of the $n+1$ bin loads obtained by starting all loads at zero and applying the preceding selection-and-increment procedure to its $n+1$ rows.

probability. For natural numbers $n,d$ and any predicate $E$ on the finite set of arrays of $n+1$ rows and $d+2$ entries per row, with each entry in $\{0,\ldots,n\}$, the probability of $E$ is the number of arrays satisfying $E$, divided in the real numbers by the total number of such arrays. This is uniform probability on all $(n+1)^{(n+1)(d+2)}$ arrays; equivalently, every individual choice is independent and uniform, with replacement.

center. For natural numbers $n,d$, the center is the real number $\log(\log(n+1))/\log(d+2)$, where $\log$ is the natural logarithm as defined by Lean’s total real logarithm. In particular, at $n=0$, its value is zero because Lean defines $\log 0=0$.

Upper. For a natural number $d$, this property means that there exists a nonnegative real constant $C$ such that for every positive real $\varepsilon$, there exists a natural number $N$ such that every natural number $n\ge N$ satisfies

Here $M_{n,d}$ is the maximum load after allocating $n+1$ balls sequentially to $n+1$ initially empty bins, each ball taking $d+2$ independent uniform choices with replacement and entering the earliest chosen bin of minimum current load. Probability is uniform counting over all complete choice arrays.

Lower. For a natural number $d$, this property means that there exists a nonnegative real constant $C$ such that for every positive real $\varepsilon$, there exists a natural number $N$ such that every natural number $n\ge N$ satisfies

Here $M_{n,d}$ is the maximum load after allocating $n+1$ balls sequentially to $n+1$ initially empty bins, using $d+2$ independent uniform choices with replacement for each ball and selecting the earliest choice of minimum current load; probability is uniform counting over the complete arrays.

TwoSided. For a natural number $d$, this property means that there exists a nonnegative real constant $C$ such that for every positive real $\varepsilon$, there exists a natural number $N$ such that every natural number $n\ge N$ satisfies

Here $M_{n,d}$ is the maximum load after allocating $n+1$ balls sequentially to $n+1$ initially empty bins, each ball making $d+2$ independent uniform choices with replacement and entering the earliest minimum-load choice; probability is uniform counting over all complete choice arrays.