Erdős Problem 50

References:

• erdosproblems.com/50
• [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
• [Sch38] Schoenberg, I. J. "On asymptotic distributions of arithmetical functions." Transactions of the American Mathematical Society 39.2 (1936): 315-330.

def Erdos50.IsDistributionOfPhiRatio (f : ℝ → ℝ) : Prop

A function $f : \mathbb{R} \to \mathbb{R}$ is the asymptotic distribution function of the values of $\varphi(n)/n$ if for all $c \in [0, 1]$, the natural density of $\{n : \varphi(n) < cn\}$ exists and equals $f(c)$.

Equations

• Erdos50.IsDistributionOfPhiRatio f = ∀ c ∈ Set.Icc 0 1, {n : ℕ | ↑n.totient < c * ↑n}.HasDensity (f c)

def Erdos50.IsPurelySingular (f : ℝ → ℝ) : Prop

A monotone function $f : \mathbb{R} \to \mathbb{R}$ is purely singular (or singular continuous) if it is continuous and its derivative equals zero almost everywhere with respect to Lebesgue measure.

Equations

• Erdos50.IsPurelySingular f = (Continuous f ∧ ∀ᵐ (x : ℝ), deriv f x = 0)

theorem Erdos50.erdos_50_schoenberg : ∃ (f : ℝ → ℝ), IsDistributionOfPhiRatio f

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$.

theorem Erdos50.erdos_50_singular (f : ℝ → ℝ) (hf : IsDistributionOfPhiRatio f) : IsPurelySingular f

Erdős [Er95] proved that the distribution function of $\varphi(n)/n$ is purely singular: it is continuous, but its derivative is zero almost everywhere.

theorem Erdos50.erdos_50 : True ↔ ∀ (f : ℝ → ℝ), IsDistributionOfPhiRatio f → ¬∃ (x : ℝ), ∃ y > 0, HasDerivAt f y x

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?