So taking we get . Additionally, if all but finitely many gaps are equal to , then exists and equals .
Taking of (1) actually shows that even the lower density is at least . The advantage of using the lower density is that it is defined for all subsets of natural numbers. Let's record this observation.
: for , , where if .
Here is another easy observation:
: If for some fixed integer , then is finite.
Proof: If is infinite, consider sets and an interval where is large enough that the smallest element of each is below . Then all disjoint sets have at least one element in , which is impossible by pigeonhole principle.
So if , then is finite – we are juggling finitely many balls. This leads to another conjecture: if , then is finite (the only difference is that now depends on ). This one is not true. Let the first set fill half of naturals, the second – half of the remaining half, etc:
Here with infinite.
So far we know that if , then is finite, but is not strong enough to guarantee that. A natural question is:
Question: is there an increasing function such that if and only if is finite? Perhaps or another polynomial?
We already saw that . So it might be fruitful to think about the (lower) densities of . Intuitively, the sum of densities of a partition cannot be larger than 1 because each density is the "proportion" of the set in . Indeed, this is easy to formally state and prove:
: if sets are disjoint, then .
Proof: It suffices to prove that for all so fix any . We have
Putting observations and together we obtain
: If is infinite, then . In particular, is asymptotically smaller than . Formally, .
See wikipedia for the and notation.
The contrapositive of the above is . Is the converse true? For example, can we find an infinite partition of with In order to answer this question I wrote a program that explores the "greedy" algorithm of making successive sets .
We want to see if we can "fit" infinitely many disjoint sets in with (starting at ). The naive greedy algorithm for doing this is as follows. Let . We now want to let but there is a collision at . So change to and keep going at strides of . In general, place the next element of , go to the current element plus the width . 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 numbers, i.e. we fill the set with sets without any problems. Additionally letting the width of be for higher constants and smaller values of suggests that this strategy is successful for for arbitrarily small. So we have the conjecture
: For any the "greedy" algorithm produces infinitely many sets with .
If this conjecture is true, then we have the following two facts:
At that point it is still unclear what happens at, say, , since converges for . But if is true, perhaps the following is true as well.
: For any increasing function such that converges, the "greedy" algorithm produces infinitely many sets with .
This would finally give the equivalence
If is finite then any sum over converges, so stating the statement above takes a bit more precision but we'll cross that bridge when we get there.
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.