Documentation

FormalConjectures.ErdosProblems.«488»

Erdős Problem 488 #

Reference: erdosproblems.com/488

theorem Erdos488.erdos_488 :
True ∀ (A : Finset ), A.Nonempty0A1A∀ (n m : ), m > nA.max n{xFinset.Icc 1 m | x {n : | n 1 aA, a n}}.card / m < 2 * {xFinset.Icc 1 n | x {n : | n 1 aA, a n}}.card / n

Let $A$ be a finite set and $$B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.$$ Is it true that, for every $m>n\geq \max(A)$, $$\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?$$