Erdős problem 697

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.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

697.lean

Retained formal statement3 of 4

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

FormalConjectures/ErdosProblems/697.leanErdos697.erdos_697.parts.ii1 lineExact file

1∀ {α : ℝ}, α < 1 / Real.log 2 → Filter.Tendsto (fun x => Erdos697.δ x α) Filter.atTop (nhds 1)

SolvedStatement only, no proof