Erdős problem 1000 · problems.science

Let $A=\{n_1<n_2<\cdots\}$ be an infinite sequence of integers, and let $\phi_A(k)$ count the number of $1\leq m\leq n_k$ such that the fraction $\frac{m}{n_k}$ does not have denominator $n_j$ for $j<k$ when written in lowest form; equivalently, $\frac{n_k}{(m,n_k)}\neq n_j$ for all $1\leq j<k$ .

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1000.lean

Retained formal statement3 of 5

In fact he proved that if $\liminf \frac{\phi_A(k)}{n_k}=0$ then $\limsup \frac{\phi_A(k)}{n_k}=1$ .

FormalConjectures/ErdosProblems/1000.leanErdos1000.erdos_1000.variants.limsup_eq_one5 linesExact file

1∀ (n : ℕ → ℕ),2  StrictMono n →3    0 < n 0 →4      Filter.liminf (fun k => ↑(Erdos1000.phiSeq n k) / ↑(n k)) Filter.atTop = 0 →5        Filter.limsup (fun k => ↑(Erdos1000.phiSeq n k) / ↑(n k)) Filter.atTop = 1

SolvedStatement only, no proof

Sources

Search problems.science