Erdős Problem 697

Reference:

• erdosproblems.com/697
• [Ha92] Hall, R. R., On some conjectures of Erdős in Astérisque. I. J. Number Theory (1992), 313--319.

theorem Erdos697.density_exists (m : ℕ) (α : ℝ) : ∃ (δ : ℝ), {n : ℕ | ∃ (d : ℕ), d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

For each $m$ and $\alpha$, the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < \exp (m ^ \alpha)$ exists.

noncomputable def Erdos697.δ (m : ℕ) (α : ℝ) : ℝ

For each $m$ and $\alpha$, $\delta (m, \alpha)$ is the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < exp (m ^ \alpha)$ exists.

Equations

• Erdos697.δ m α = ⋯.choose

theorem Erdos697.erdos_697.delta_lt (m : ℕ) (α : ℝ) : δ m α < (↑m ^ α + 1) / ↑m

$\delta < \frac{m ^ \alpha + 1}{m}`. This shows that $lim_{m\rightarrow\infty} \delta (m, \alpha) = 0$ for $\alpha < 1$. #TODO: prove this theorem.

theorem Erdos697.erdos_697.beta_lt {α : ℝ} (hα : 1 / Real.log 2 < α) : Filter.Tendsto (fun (x : ℕ) => δ x α) Filter.atTop (nhds 0)

Let $\beta = \frac{1}{\log 2}$. Then $lim_{m\rightarrow\infty} \delta (m, \alpha) = 0$ if $\alpha < \beta$. This is proved in [Ha92].

theorem Erdos697.erdos_697.lt_beta {α : ℝ} (hα : α < 1 / Real.log 2) : Filter.Tendsto (fun (x : ℕ) => δ x α) Filter.atTop (nhds 1)

$lim_{m\rightarrow\infty} \delta (m, \alpha) = 1$ if $\beta < \alpha$. This is proved in [Ha92].