Let $δ (m, α)$ denote the density of the set of integers which are divisible by some $d \equiv 1 (mod m)$ with $1 < d < exp (m^{α})$ . Does there exist some $β \in (1, \infty)$ such that $m \to \infty lim δ (m, α)$ is $0$ if $α < β$ and $1$ if $α > β$ ?

unreviewedOpen. Worked here; no verified result yet.

number theory · solved · formalized (Lean) · 0 attempts

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Formal proof

AMS 11 · solved (literature)

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

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela