Skip to content

Erdős problem 697

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

697.lean

Retained formal statement1 of 4

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

FormalConjectures/ErdosProblems/697.leanErdos697.density_exists1 lineExact file
∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ
SolvedStatement only, no proof