Erdős problem 1000
Let be an infinite sequence of integers, and let count the number of such that the fraction does not have denominator for when written in lowest form; equivalently, for all .
Sources
FormalConjectures/ErdosProblems/
1000.lean
Retained formal statement
The study of was introduced by Cassels [Ca50b], who proved that there exist sequences such that
∃ n, StrictMono n ∧ 0 < n 0 ∧ Filter.liminf (Erdos1000.phiAvg n) Filter.atTop = 0SolvedStatement only, no proof