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 statement2 of 4

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

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

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

SolvedStatement only, no proof