Erdős Problem 416

Reference: erdosproblems.com/416

@[reducible, inline]

noncomputable abbrev Erdos416.V (x : ℝ) : ℝ

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable

Equations

• Erdos416.V x = ↑(Finset.filter (fun (n : ℕ) => ∃ (m : ℕ), m.totient = n) (Finset.Icc 1 ⌊x⌋₊)).card

theorem Erdos416.erdos_416.parts.i : Filter.Tendsto (fun (x : ℝ) => V (2 * x) / V x) Filter.atTop (nhds 2)

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2 ?

theorem Erdos416.erdos_416.parts.ii : let f := sorry; Filter.Tendsto (fun (x : ℝ) => V x / f x) Filter.atTop (nhds 1)

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Is there an asymptotic formula for V(x)?

theorem Erdos416.erdos_416.variants.Pillai : V =o[Filter.atTop] id

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Pillai proved V(x)=o(x). Ref: S. Sivasankaranarayana Pillai, On some functions connected with $\phi(n)$

theorem Erdos416.erdos_416.variants.Erdos : ∃ (f : ℝ → ℝ), f =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, V x = x * Real.log x ^ (-1 + f x)

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Erdős proved V(x)=x(logx)^(−1+o(1)). Ref: Erdős, P., On the normal number of prime factors of $p-1$ and some related problems concerning Euler's $\varphi$-function.

theorem Erdos416.erdos_416.variants.Maier_Pomerance : let C := sorry; 0 < C ∧ ∃ (f : ℝ → ℝ), f =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, V x = x / Real.log x * Real.exp ((C + f x) * Real.log (Real.log (Real.log x)) ^ 2)

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x)=x/logx * e^((C+o(1))(log log log x)^2), for some explicit constant C>0. Ref:Maier, Helmut and Pomerance, Carl, On the number of distinct values of Euler's $\phi$-function.

theorem Erdos416.erdos_416.variants.Ford : match sorry with | (C₁, C₂, C₃) => 0 < C₁ ∧ 0 < C₂ ∧ 0 < C₃ ∧ let G := fun (x : ℝ) => x / Real.log x * Real.exp (C₁ * (Real.log (Real.log (Real.log x)) - Real.log (Real.log (Real.log (Real.log x)))) ^ 2 + C₂ * Real.log (Real.log (Real.log x)) - C₃ * Real.log (Real.log (Real.log (Real.log x)))); V =Θ[Filter.atTop] G

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x) ≍ x/log x*e^(C_1*(log log log x − log log log log x)^2+C_2 log log log x − C_3 log log log log x) Ref: Ford, Kevin, The distribution of totients.