Erdős Problem 351

Reference: erdosproblems.com/351

def Erdos351.imageSet {α : Type u_1} [Semifield α] (P : Polynomial α) : Set α

The set of rational numbers of the form P(n) + 1 / n where n is a natural number and P is a polynomial with rational coefficients.

Equations

• Erdos351.imageSet P = Set.range fun (n : ℕ) => Polynomial.eval (↑n) P + 1 / ↑n

def Erdos351.IsStronglyComplete {α : Type u_1} [Semiring α] (A : Set α) : Prop

The predicate that a set A is strongly complete, i.e. that for every finite set B, every sufficiently large integer is a sum of elements of the set A \ B.

Equations

• Erdos351.IsStronglyComplete A = ∀ (B : Finset α), ∀ᶠ (m : ℕ) in Filter.atTop, ↑m ∈ {x : α | ∃ (X : Finset α) (_ : ↑X ⊆ A \ ↑B), ∑ n ∈ X, n = x}

def Erdos351.HasCompleteImage (P : Polynomial ℚ) : Prop

The predicate that rational polynomial P has a complete image.

Equations

• Erdos351.HasCompleteImage P = Erdos351.IsStronglyComplete (Erdos351.imageSet P)

theorem Erdos351.erdos_351 : (∀ (P : Polynomial ℚ), HasCompleteImage P) ↔ sorry

Let $p(x)\in \mathbb{Q}[x]$. Is it true that [A={ p(n)+1/n : n\in \mathbb{N}}] is strongly complete, in the sense that, for any finite set $B$, [\left{\sum_{n\in X}n : X\subseteq A\backslash B\textrm{ finite }\right}] contains all sufficiently large rational numbers?

theorem Erdos351.erdos_351.variants.X : HasCompleteImage Polynomial.X

Let $p(x) = x\in \mathbb{Q}[x]$. It has been shown that [A={ p(n)+1/n : n\in \mathbb{N}}] is strongly complete, in the sense that, for any finite set $B$, [\left{\sum_{n\in X}n : X\subseteq A\backslash B\textrm{ finite }\right}] contains all sufficiently large rational numbers.