Erdős Problem 1060

Reference: erdosproblems.com/1060

theorem Erdos1060.erdos_1060.bound_one : ∃ (h : ℕ → ℝ), (h =o[Filter.atTop] fun (n : ℕ) => 1 / Real.log (Real.log ↑n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card ≤ ↑n ^ h n

The conjecture is about the function $f(n)$ which counts the number of solutions to $k\sigma(k)=n$, where $\sigma(k)$ is the sum of divisors of $k$. The first bound is that $f(n)$ grows slower than any power of $n^(\frac{1}{\log\log n})$. The second bound is that $f(n)$ is at most a power of $\log n$.

theorem Erdos1060.erdos_1060.bound_two : ∃ (C : ℝ), (fun (n : ℕ) => ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card) =O[Filter.atTop] fun (n : ℕ) => Real.log ↑n ^ C