Erdős problem 448
Let count the divisors of and count the number of such that has a divisor in . Is it true that, for all , for almost all ?
Sources
FormalConjectures/ErdosProblems/
448.lean
Let count the divisors of and count the number of such that has a divisor in . Is it true that, for all , for almost all ?
This is false, and was disproved by Erdős and Tenenbaum [ErTe81], who showed that in fact the upper density of the set of such is (where the in the exponent as ). A more precise result was proved by Hall and Tenenbaum [HaTe88] (see Section 4.6), who showed that the upper density is . Hall and Tenenbaum further prove that has a distribution function. Erdős and Graham also asked whether there is a good inequality known for . This was provided by Ford [Fo08] who proved where
False ↔ ∀ (ε : ℝ), 0 < ε → {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1