Strongly complete sequences

3 fully proved1 ready to prove

Strongly complete sets

DefinitionStrongly complete sets of rationals#✓fully proved

A set \(A\) of rational numbers is strongly complete when, for every finite set \(B\) of rational numbers, there is an integer \(N_0\) such that every integer \(m \ge N_0\) is the sum of the elements of some finite subset of \(A \setminus B\).

def StronglyComplete (A : Set ℚ) : Prop :=
  ∀ B : Set ℚ, B.Finite →
    ∃ N₀ : ℤ, ∀ m : ℤ, N₀ ≤ m →
      (m : ℚ) ∈ { s : ℚ | ∃ X : Finset ℚ, (↑X : Set ℚ) ⊆ A \ B ∧ ∑ a ∈ X, a = s }

Used by 1

Used byThe strong completeness statement of Erdős Problem 351

DefinitionPolynomial values plus reciprocals#✓fully proved

For a polynomial \(p\) with rational coefficients, \(A_p\) is the set of rational numbers \(p(n) + 1/n\), where \(n\) ranges over the positive integers.

def ErdosSet351 (p : Polynomial ℚ) : Set ℚ :=
  { q : ℚ | ∃ n : ℕ, n ≠ 0 ∧ q = p.eval (n : ℚ) + 1 / (n : ℚ) }

Used by 1

Used byThe strong completeness statement of Erdős Problem 351

DefinitionThe strong completeness statement of Erdős Problem 351#✓fully proved

This is the proposition that for every polynomial \(p\) with rational coefficients and positive leading coefficient, the set \(A_p\) of rational numbers \(p(n) + 1/n\), where \(n\) ranges over the positive integers, is strongly complete.

def StrongCompletenessQuestion : Prop :=
  ∀ p : Polynomial ℚ, 0 < p.leadingCoeff → StronglyComplete (ErdosSet351 p)

def StronglyComplete (A : Set ℚ) : Prop :=
  ∀ B : Set ℚ, B.Finite →
    ∃ N₀ : ℤ, ∀ m : ℤ, N₀ ≤ m →
      (m : ℚ) ∈ { s : ℚ | ∃ X : Finset ℚ, (↑X : Set ℚ) ⊆ A \ B ∧ ∑ a ∈ X, a = s }

WantedExt/NumberTheory/ErdosProblem351Wanted.lean:44

def ErdosSet351 (p : Polynomial ℚ) : Set ℚ :=
  { q : ℚ | ∃ n : ℕ, n ≠ 0 ∧ q = p.eval (n : ℚ) + 1 / (n : ℚ) }

WantedExt/NumberTheory/ErdosProblem351Wanted.lean:50

Uses 2 · Used by 1

Statement usesPolynomial values plus reciprocals · Strongly complete sets of rationals

Used byStrong completeness of polynomial values plus reciprocals (Erdős Problem 351)

Erdős Problem 351

TheoremStrong completeness of polynomial values plus reciprocals (Erdős Problem 351)#●ready to prove

For every polynomial \(p\) with rational coefficients and positive leading coefficient, let \(A_p\) be the set of rational numbers \(p(n) + 1/n\), where \(n\) ranges over the positive integers. Then \(A_p\) is strongly complete: for every finite set \(B\) of rational numbers there is an integer \(N_0\) such that every integer \(m \ge N_0\) is the sum of the elements of some finite subset of \(A_p \setminus B\).

Resolved true: The maintained Erdős Problems page marks Problem 351 proved in the affirmative and records that the positive solution follows from the positive solution of Problem 283.

public theorem_wanted StrongCompletenessQuestion_holds : EP351.StrongCompletenessQuestion

Sources

plby/lean-proofs, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/Util/PolynomialEgyptianSums.lean#L10266.

Uses 1

Statement usesThe strong completeness statement of Erdős Problem 351

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.