1. Mathematical observations
    1. Width and density
    2. Growth of w(On)w(\mathcal O_n)
  2. Programming exploration
    1. Greedy approach
    2. Formalization in Lean

A puzzle

The other day my friend Leo presented the following puzzle to me. Given a partition {On}nI\left\{ \mathcal O_n \right\}_{n\in I} of positive integers with On\mathcal O_n all infinite, find a condition that is equivalent to II finite. The motivation for the problem was juggling: each On\mathcal O_n is the "orbit" of the nthn^{\text{th}} ball, and we want to know when we are juggling finitely many balls.

Mathematical observations

Width and density

After playing around with some examples we came up with the definition of width of an infinite subset of Z+\mathbb Z_+: the width of O\mathcal O denoted by w(O)w(\mathcal O) is the supremum of distances between consecutive elements. Intuitively, width is kind of the reciprocal of natural density. Recall that the natural density of O\mathcal O is the limit d(O)=limna(n)/nd(\mathcal O) = \lim_{n\to \infty} a(n)/n where a(n)a(n) is the number of elements of O\mathcal O in {1,...,n}\left\{ 1,...,n \right\}. Therefore 1/w(O)d(O)1/w(\mathcal O) \leq d(\mathcal O). Let's see why that is.

Given O={xi}1Z+\mathcal O = \left\{ x_i \right\}_1^\infty \subset \mathbb Z_+, let y0=x1y_0 = x_1 and yi=xi+1xiy_i = x_{i+1} - x_i so that yiy_i's are the "gaps" between consecutive terms of the sequence O\mathcal O. Then w(O)=sup{yi:i1}w(\mathcal O) = \sup \left\{ y_i: i\geq 1 \right\}. On the other hand, for n=xin = x_i

a(n)/n=i/xibecause a(xi)=i=ij=1iyjij=1iw(O)=1/w(O).\begin{aligned} a(n)/n &= i/x_i \text{\hspace{2cm} because $a(x_i) = i$}\\ &= \frac{i}{\sum_{j=1}^i y_j} \geq \frac{i}{\sum_{j=1}^i w(\mathcal O)} = 1/w(\mathcal O). \end{aligned}

So taking limi\lim_i \to \infty we get d(O)1/w(O)d(\mathcal O) \geq 1/w(\mathcal O). Additionally, if all but finitely many gaps yiy_i are equal to w(O)w(\mathcal O), then d(O)d(\mathcal O) exists and equals 1/w(O)1/w(\mathcal O).

Taking lim infi\liminf_{i\to\infty} of (1) actually shows that even the lower density d(O)=lim infna(n)/n\underline{d}(\mathcal O) = \liminf_n a(n)/n is at least 1/w(O)1/w(\mathcal O). The advantage of using the lower density is that it is defined for all subsets of natural numbers. Let's record this observation.

O1O_1: for OZ+\mathcal O \subset \mathbb Z_+, 1/w(O)d(O)1/w(\mathcal O) \leq \underline{d}(\mathcal O), where 1/w(O)=01/w(\mathcal O)=0 if w(O)=w(\mathcal O) = \infty.

Growth of w(On)w(\mathcal O_n)

Here is another easy observation:

O2O_2: If nI,w(On)M\forall n \in I, w(\mathcal O_n) \leq M for some fixed integer MM, then II is finite.

Proof: If II is infinite, consider M+1M+1 sets O1,...,OM+1\mathcal O_1,...,\mathcal O_{M+1} and an interval [a,a+M1][a,a+M-1] where aa is large enough that the smallest element of each On,nM+1\mathcal O_n, n\leq M+1 is below aa. Then all M+1M+1 disjoint sets O1,...,OM+1\mathcal O_1,...,\mathcal O_{M+1} have at least one element in [a,a+M1][a,a+M-1], which is impossible by pigeonhole principle.

So if w(On)=O(1)w(\mathcal O_n) = O(1), then II is finite – we are juggling finitely many balls. This leads to another conjecture: if nI,w(On)Mn\forall n \in I, w(\mathcal O_n) \leq M_n, then II is finite (the only difference is that now MnM_n depends on nn). This one is not true. Let the first set fill half of naturals, the second – half of the remaining half, etc:

O1=2Z+, O2=1+4Z+, O3=3+8Z+, ..., On=2n11+2nZ+.\mathcal O_1 = 2\mathbb Z_+,\ \mathcal O_2 = 1 + 4\mathbb Z_+,\ \mathcal O_3 = 3+8\mathbb Z_+,\ ... ,\ \mathcal O_n = 2^{n-1}-1 + 2^n\mathbb Z_+.

Here w(On)=2nw(\mathcal O_n) = 2^n with II infinite.

So far we know that if w(On)=O(1)w(\mathcal O_n) = O(1), then II is finite, but w(On)=O(2n)w(\mathcal O_n) = O(2^n) is not strong enough to guarantee that. A natural question is:

Question: is there an increasing function f(n)f(n) such that w(On)=O(f(n))w(\mathcal O_n) = O(f(n)) if and only if II is finite? Perhaps f(n)=n2f(n) = n^2 or another polynomial?

We already saw that 1/w(O)d(O)1/w(\mathcal O) \leq \underline{d}(\mathcal O). So it might be fruitful to think about the (lower) densities of On\mathcal O_n. Intuitively, the sum of densities of a partition cannot be larger than 1 because each density is the "proportion" of the set in Z+\mathbb Z_+. Indeed, this is easy to formally state and prove:

O3O_3: if sets {On}n=1\left\{ \mathcal O_n \right\}_{n=1}^\infty are disjoint, then n=1d(On)1\sum_{n=1}^\infty \underline{d}(\mathcal O_n) \leq 1.

Proof: It suffices to prove that n=1Nd(On)1\sum_{n=1}^N \underline{d}(\mathcal O_n) \leq 1 for all NN so fix any NN. We have

n=1Nd(On)=lim infin=1NOn[i]i=lim infi1in=1NOn[i]lim infi1i×i=1 because On’s are disjoint.\begin{aligned} \sum_{n=1}^N \underline{d}(\mathcal O_n) &= \liminf_{i\to\infty} \sum_{n=1}^N \frac{|\mathcal O_n\cap [i]|}{i} = \liminf_{i\to\infty} \frac{1}{i}\sum_{n=1}^N |\mathcal O_n\cap [i]|\\ &\leq \liminf_{i\to\infty} \frac{1}{i}\times i = 1 \text{ \hspace{1cm} because $\mathcal O_n$'s are disjoint}. \end{aligned}

Putting observations O1O_1 and O3O_3 together we obtain

O4O_4: If II is infinite, then n=11/w(On)1\sum_{n=1}^\infty 1/w(\mathcal O_n) \leq 1. In particular, 1/w(On)1/w(\mathcal O_n) is asymptotically smaller than 1/n1/n. Formally, w(On)=ω(n)w(\mathcal O_n) = \omega(n).

See wikipedia for the ω\omega and Ω\Omega notation.

The contrapositive of the above is w(On)=O(n) I<w(\mathcal O_n) = O(n) \implies |I| < \infty. Is the converse true? For example, can we find an infinite partition {On}\left\{ \mathcal O_n \right\} of Z+\mathbb Z_+ with w(On)n2?w(\mathcal O_n) \leq n^2? In order to answer this question I wrote a program that explores the "greedy" algorithm of making successive sets On\mathcal O_n.

Programming exploration

Greedy approach

We want to see if we can "fit" infinitely many disjoint sets {On}\left\{ \mathcal O_n \right\} in Z+\mathbb Z_+ with w(On)n2w(\mathcal O_n) \leq n^2 (starting at n=2n=2). The naive greedy algorithm for doing this is as follows. Let O2=4,8,12,16,etc\mathcal O_2 = 4,8,12,16,\text{etc}. We now want to let O3=9,18,27,36,etc.\mathcal O_3 = 9,18,27,36,\text{etc.} but there is a collision at 3636. So change 3636 to 3535 and keep going at strides of 99. In general, place the next element of On\mathcal O_n, go to the current element plus the width n2n^2. If this spot is empty, put it there, if not, try the spot one below, etc. If we are ever unable to find the next spot because on our search down we returned back to the current element, then this strategy fails. If no such failure occurs, then we succeed.

The aforementioned program successfully uses this strategy for 10810^8 numbers, i.e. we fill the set {1,,108}\left\{ 1,\dots,10^8 \right\} with sets O2,,O108\mathcal O_2,\dots,\mathcal O_{\sqrt{10^8}} without any problems. Additionally letting the width of On\mathcal O_n be cn1+ϵc \cdot n^{1+\epsilon} for higher constants cc and smaller values of ϵ>0\epsilon>0 suggests that this strategy is successful for w(On)=Θ(n1+ϵ)w(\mathcal O_n) = \Theta(n^{1+\epsilon}) for ϵ>0\epsilon>0 arbitrarily small. So we have the conjecture

C1C_1: For any ϵ>0\epsilon>0 the "greedy" algorithm produces infinitely many sets On\mathcal O_n with w(On)=Θ(n1+ϵ)w(\mathcal O_n) = \Theta(n^{1+\epsilon}).

If this conjecture is true, then we have the following two facts:

  1. I= w(On)=ω(n)|I| = \infty \implies w(\mathcal O_n) = \omega(n).

  2. w(On)=Ω(n1+ϵ) I=w(\mathcal O_n) = \Omega(n^{1+\epsilon}) \implies |I| = \infty.

At that point it is still unclear what happens at, say, w(On)=Θ(nlog2n)w(\mathcal O_n) = \Theta(n\log^2 n), since 1nlogkn\sum \frac{1}{n\log^k n} converges for k>1k>1. But if C1C_1 is true, perhaps the following is true as well.

C2C_2: For any increasing function ff such that n1/f(n)\sum_n 1/f(n) converges, the "greedy" algorithm produces infinitely many sets On\mathcal O_n with w(On)=Θ(f(n))w(\mathcal O_n) = \Theta(f(n)).

This would finally give the equivalence

I= nI1/w(On)<.|I|=\infty \iff \sum_{n\in I} 1/w(\mathcal O_n) < \infty.

If II is finite then any sum over nIn\in I converges, so stating the statement above takes a bit more precision but we'll cross that bridge when we get there.

Formalization in Lean

Lean is a proof assistant that allows people to "explain" mathematics to a computer. For example, here is my proof of the squeeze theorem. It would be cool to formalize the above observations in Lean.