Erdős Problem 1064

Reference: erdosproblems.com/1064

theorem Erdos1064.erdos_1064 : {n : ℕ | n.totient > (n - n.totient).totient}.HasDensity 1

Let $ϕ(n)$ be the Euler's totient function, then the $n$ satisfies $ϕ(n)>ϕ(n - ϕ(n))$ have asymptotic density 1. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rd\H os concerning the arithmetical functions {$\phi$} and {$\sigma$}. Colloq. Math.

theorem Erdos1064.erdos_1064.variants.k2 : {n : ℕ | n.totient < (n - n.totient).totient}.Infinite

Let $ϕ(n)$ be the Euler's totient function, there exist infinitely many $n$ such that $ϕ(n)< ϕ(n - ϕ(n))$ Reference: [GLW01] Grytczuk, A. and Luca, F. and W'ojtowicz, M., A conjecture of {E}rdős concerning inequalities for the {E}uler totient function.

theorem Erdos1064.erdos_1064.variants.general_function (f : ℕ → ℕ) (hf : (fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : {n : ℕ | (n - n.totient).totient + f n < n.totient}.HasDensity 1

For any function $f(n)=o(n)$, we have $\phi(n)>\phi(n-\phi(n))+f(n)$ for almost all $n$. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rd\H os concerning the arithmetical functions {$\phi$} and {$\sigma$}. Colloq. Math. (2002), 111--130.