Documentation

FormalConjectures.ErdosProblems.«1210»

Erdős Problem 1210 #

References:

theorem Erdos1210.erdos_1210 :
True ∃ (C : ), ∀ (n : ) (A : Finset ), (∀ aA, 1 a a < n)(∀ aA, bA, a ba.Coprime b)aA, 1 / (n - a) pFinset.range n with Prime p, 1 / p + C

Let $A\subseteq [1,n)$ be a set of integers such that $(a,b)=1$ for all distinct $a,b\in A$. Is it true that $\sum_{a\in A}\frac{1}{n-a}\leq \sum_{p < n}\frac{1}{p}+O(1)$?

theorem Erdos1210.erdos_1210.variants.er80_correction :
True ∃ (C : ), ∀ (n m : ), n < mqFinset.Ioc n m with Prime q, 1 / (q - n) < pFinset.range (m - n) with Prime p, 1 / p + C

In [Er80] he claims he "did not state this quite correctly" in [Er77c]. The problem in [Er77c] which Erdős is presumably referring to states that if $n < q_1 < \cdots < q_k\leq m$ is the set of primes in $(n,m]$ then $\sum \frac{1}{q_i-n} < \sum_{p < m-n}\frac{1}{p}+O(1)$.