Erdős Problem 448

References:

• erdosproblems.com/448
• [Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70.
• [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82.
• [HaTe88] Hall, Richard R. and Tenenbaum, Gérald, Divisors. (1988), xvi+167.
• [ErTe81] Erdős, P., Tenenbaum, G., Sur la structure de la suite des diviseurs d'un entier. Ann. Inst. Fourier (Grenoble) 31 (1981), 17–37.
• [Fo08] Ford, Kevin, The distribution of integers with a divisor in a given interval. Ann. of Math. (2) 168 (2008), 367–433.

def Erdos448.tauPlus (n : ℕ) : ℕ

tauPlus n (written $\tau^+(n)$) counts the number of $k$ such that $n$ has a divisor in $[2^k, 2^{k+1})$. Equivalently, the number of distinct values $\lfloor \log_2 d \rfloor$ as $d$ ranges over the divisors of $n$: a divisor $d$ lies in $[2^k, 2^{k+1})$ iff Nat.log 2 d = k.

Equations

• Erdos448.tauPlus n = (Finset.image (Nat.log 2) n.divisors).card

theorem Erdos448.tauPlus_six : tauPlus 6 = 3

Sanity check: $\tau^+(6) = 3$. Divisors $1, 2, 3, 6$ lie in dyadic blocks $k = 0, 1, 1, 2$, so the distinct blocks are $\{0, 1, 2\}$. ($\tau(6) = 4$.)

theorem Erdos448.tauPlus_twelve : tauPlus 12 = 4

Sanity check: $\tau^+(12) = 4$. Divisors $1, 2, 3, 4, 6, 12$ lie in dyadic blocks $k = 0, 1, 1, 2, 2, 3$, so the distinct blocks are $\{0, 1, 2, 3\}$. ($\tau(12) = 6$.)

theorem Erdos448.tauPlus_le_tau (n : ℕ) : tauPlus n ≤ n.divisors.card

Always $\tau^+(n) \le \tau(n)$: the occupied dyadic blocks are the image of the divisor set under Nat.log 2, and an image has at most as many elements as its source. This is what makes the $\epsilon < 1$ comparison in the problem meaningful.

theorem Erdos448.erdos_448 : False ↔ ∀ (ε : ℝ), 0 < ε → {n : ℕ | ↑(tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1

Let $\tau(n)$ count the divisors of $n$ and $\tau^+(n)$ count the number of $k$ such that $n$ has a divisor in $[2^k, 2^{k+1})$. Is it true that, for all $\epsilon > 0$, $$ \tau^+(n) < \epsilon \cdot \tau(n) $$ for almost all $n$?

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 $n$ is $\asymp \epsilon^{1-o(1)}$ (where the $o(1)$ in the exponent $\to 0$ as $\epsilon \to 0$). A more precise result was proved by Hall and Tenenbaum [HaTe88] (see Section 4.6), who showed that the upper density is $\ll \epsilon \log(2/\epsilon)$. Hall and Tenenbaum further prove that $\tau^+(n)/\tau(n)$ has a distribution function. Erdős and Graham also asked whether there is a good inequality known for $\sum_{n \leq x} \tau^+(n)$. This was provided by Ford [Fo08] who proved $$ \sum_{n \leq x} \tau^+(n) \asymp x\frac{(\log x)^{1-\alpha}}{(\log\log x)^{3/2}} $$ where $$ \alpha = 1-\frac{1+\log\log 2}{\log 2} = 0.08607\cdots. $$

theorem Erdos448.erdos_448.variants.erdos_tenenbaum : Filter.Tendsto (fun (ε : ℝ) => Real.log {n : ℕ | ↑(tauPlus n) < ε * ↑n.divisors.card}.upperDensity / Real.log ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Quantitative form of the (negative) answer to erdos_448. Erdős and Tenenbaum [ErTe81] showed that the upper density of $\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}$ is in fact $\asymp \epsilon^{1 - o(1)}$, where the $o(1)$ in the exponent tends to $0$ as $\epsilon \to 0$. Equivalently, $\log(\text{upper density}) / \log \epsilon \to 1$ as $\epsilon \to 0^+$.

theorem Erdos448.erdos_448.variants.hall_tenenbaum_upper_bound : (fun (ε : ℝ) => {n : ℕ | ↑(tauPlus n) < ε * ↑n.divisors.card}.upperDensity) =O[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ε * Real.log (2 / ε)

A more precise result of Hall and Tenenbaum [HaTe88, §4.6]: the upper density of $\{n : \tau^+(n) < \epsilon \cdot \tau(n)\}$ is $\ll \epsilon \cdot \log(2/\epsilon)$ as $\epsilon \to 0^+$.

theorem Erdos448.erdos_448.variants.hall_tenenbaum_distribution : ∃ (F : ℝ → ℝ), ∀ (z : ℝ), {n : ℕ | ↑(tauPlus n) / ↑n.divisors.card ≤ z}.HasDensity (F z)

Hall and Tenenbaum [HaTe88] further prove that $\tau^+(n)/\tau(n)$ has a distribution function: there is a function F such that, for every $z$, the set $\{n : \tau^+(n)/\tau(n) \le z\}$ has density F z.

theorem Erdos448.erdos_448.variants.ford : (fun (x : ℕ) => ∑ n ∈ Finset.Icc 1 x, ↑(tauPlus n)) =Θ[Filter.atTop] fun (x : ℕ) => have α := 1 - (1 + Real.log (Real.log 2)) / Real.log 2; ↑x * Real.log ↑x ^ (1 - α) / Real.log (Real.log ↑x) ^ (3 / 2)

Erdős and Graham asked whether there is a good inequality for $\sum_{n \le x} \tau^+(n)$. This was answered by Ford [Fo08], who proved $$ \sum_{n \le x} \tau^+(n) \asymp x \cdot \frac{(\log x)^{1 - \alpha}}{(\log\log x)^{3/2}}, $$ where $\alpha = 1 - \frac{1 + \log\log 2}{\log 2} = 0.08607\ldots$.