Erdős problem 450 · problems.science

How large must $y(\varepsilon, n)$ be so that every interval $(x, x+y)$ contains at most $\varepsilon y$ integers having a divisor in $(n, 2n)$ ? The candidate proof gives the sharp fixed- $\varepsilon$ order $y = \Theta_\varepsilon(n)$ , uniformly in the translate.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

450.lean

Retained formal statement1 of 2

How large must $y=y(\epsilon,n)$ be such that the number of integers in $(x,x+y)$ with a divisor in $(n,2n)$ is at most $\epsilon y$ ?

A linear scale is known to suffice (see erdos_450.linear_scale_suffices). Whether the optimal scale is *sublinear* — a sufficient Y with Y ε n = o(n) — is open.

FormalConjectures/ErdosProblems/450.leanErdos450.erdos_4502 linesExact file

1True ↔2  ∃ Y, Erdos450.IsSufficientScale Y ∧ ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun n => ↑(Y ε n) / ↑n) Filter.atTop (nhds 0)

OpenStatement only, no proof

Sources

Search problems.science