Erdős problem 413

Erdős proved that the barrier set for expProd is infinite and even has positive density.

HasPosDensity is the right reading rather than positive lower density. In [Er79d] this is Theorem 1, "the density of integers satisfying (2) is positive", where d₀(n) = ∏ αᵢ is expProd. The averaging argument there bounds the density below, but Erdős states the existence separately on the last page: "With a little more trouble, I can prove that the density of integers n for which n is a barrier for d₀(n) exists." He goes further, that if αᵢ is the density of n with max_{m<n} (m + d₀(m)) = n + i, then every αᵢ exists and they sum to 1.

[Er79d] Erdős, P., *Some unconventional problems in number theory*. Acta Math. Acad. Sci. Hungar. (1979), 71-80.