Erdős problem 50

Schoenberg [Sch38] proved that the asymptotic distribution function of $\varphi(n)/n$ exists. That is, for any $c \in [0, 1]$ , the proportion of integers $n \le N$ satisfying $\varphi(n)/n < c$ approaches a limit as $N \to \infty$ . This limit function is the cumulative distribution function of the values of $\varphi(n)/n$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

50.lean

Retained formal statement1 of 3

Let $f$ be the asymptotic distribution function of $\varphi(n)/n$ , so that for each $c \in [0,1]$ , $f(c)$ is the natural density of $\{n : \varphi(n) < cn\}$ . Is it true that there is no $x$ such that the derivative $f'(x)$ exists and is positive?

FormalConjectures/ErdosProblems/50.leanErdos50.erdos_502 linesExact file

1sorry ↔2  ∀ (f : ℝ → ℝ), Erdos50.IsDistributionOfPhiRatio f → ¬∃ x ∈ Set.Icc 0 1, ∃ y > 0, HasDerivWithinAt f y (Set.Icc 0 1) x

OpenStatement only, no proof